def HighDimensional.IsCLipschitz {α : Type u_1} {β : Type u_2} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (c : ℝ) (f : α → β) : Prop

structure HighDimensional.IsDEmbedding {X : Type u_1} [MetricSpace X] [Fintype X] {k : ℕ} (D : ℝ) (f : X → EuclideanSpace ℝ (Fin k)) : Prop

• one_lipschitz (x y : X) : ‖f x - f y‖ ≤ dist x y
• distortion_bound (x y : X) : dist x y ≤ D * ‖f x - f y‖

@[reducible, inline]

abbrev HighDimensional.UnitSphere (n : ℕ) : Type

@[implicit_reducible]

instance HighDimensional.instMeasurableSpaceUnitSphere (n : ℕ) : MeasurableSpace (UnitSphere n)

noncomputable def HighDimensional.sphereMeasure (n : ℕ) : MeasureTheory.Measure (UnitSphere n)

noncomputable def HighDimensional.uniformSphereMeasure (n : ℕ) : MeasureTheory.Measure (UnitSphere n)

def HighDimensional.IsMedian {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → ℝ) (M : ℝ) : Prop

noncomputable def HighDimensional.projFirstK (n k : ℕ) (hk : k ≤ n) (x : EuclideanSpace ℝ (Fin n)) : EuclideanSpace ℝ (Fin k)

noncomputable def HighDimensional.normProjFirstK (n k : ℕ) (hk : k ≤ n) (x : EuclideanSpace ℝ (Fin n)) : ℝ

noncomputable def HighDimensional.sphereProjNorm (n k : ℕ) (hk : k ≤ n) : UnitSphere n → ℝ

theorem HighDimensional.projFirstK_lipschitz (n k : ℕ) (hk : k ≤ n) (x y : EuclideanSpace ℝ (Fin n)) : ‖projFirstK n k hk x - projFirstK n k hk y‖ ≤ ‖x - y‖

theorem HighDimensional.sphereProjNorm_lipschitzWith (n k : ℕ) (hk : k ≤ n) : LipschitzWith 1 (sphereProjNorm n k hk)

theorem HighDimensional.isoperimetric_sphere_one_sided (n : ℕ) (ε : ℝ) (hε : 0 < ε) (A : Set (UnitSphere n)) (hA : (uniformSphereMeasure n) A ≥ (uniformSphereMeasure n) Set.univ / 2) : (uniformSphereMeasure n) (Metric.cthickening ε A)ᶜ ≤ ENNReal.ofReal (Real.exp (-(↑n * ε ^ 2 / 2)))

theorem HighDimensional.cthickening_sublevel_of_lipschitz {α : Type u_1} [PseudoMetricSpace α] (f : α → ℝ) (hf : LipschitzWith 1 f) (M ε : ℝ) (hε : 0 ≤ ε) (hne : {x : α | f x ≤ M}.Nonempty) : Metric.cthickening ε {x : α | f x ≤ M} ⊆ {x : α | f x ≤ M + ε}

theorem HighDimensional.cthickening_superlevel_of_lipschitz {α : Type u_1} [PseudoMetricSpace α] (f : α → ℝ) (hf : LipschitzWith 1 f) (M ε : ℝ) (hε : 0 ≤ ε) (hne : {x : α | f x ≥ M}.Nonempty) : Metric.cthickening ε {x : α | f x ≥ M} ⊆ {x : α | f x ≥ M - ε}

theorem HighDimensional.concentration_lipschitz_sphere (n : ℕ) (f : UnitSphere n → ℝ) (hf : LipschitzWith 1 f) (M : ℝ) (hM : IsMedian (uniformSphereMeasure n) f M) (ε : ℝ) (hε : 0 < ε) (hne_low : {x : UnitSphere n | f x ≤ M}.Nonempty) (hne_high : {x : UnitSphere n | f x ≥ M}.Nonempty) : (uniformSphereMeasure n) {x : UnitSphere n | ε < |f x - M|} ≤ ENNReal.ofReal (2 * Real.exp (-(↑n * ε ^ 2 / 2)))

theorem HighDimensional.concentration_projection_sphere (n k : ℕ) (hk : k ≤ n) (M : ℝ) (hM : IsMedian (uniformSphereMeasure n) (sphereProjNorm n k hk) M) (t : ℝ) (ht : 0 < t) (hne_low : {x : UnitSphere n | sphereProjNorm n k hk x ≤ M}.Nonempty) (hne_high : {x : UnitSphere n | sphereProjNorm n k hk x ≥ M}.Nonempty) : (uniformSphereMeasure n) {x : UnitSphere n | t < |sphereProjNorm n k hk x - M|} ≤ ENNReal.ofReal (2 * Real.exp (-(t ^ 2 * ↑n / 2)))

theorem HighDimensional.sphere_shell_bm_bound (n : ℕ) (ε : ℝ) (hε : 0 < ε) (A : Set (UnitSphere n)) (hA : (uniformSphereMeasure n) A ≠ 0) (hA_small : (uniformSphereMeasure n) A < (uniformSphereMeasure n) Set.univ / 2) : (uniformSphereMeasure n) (Metric.thickening ε A)ᶜ ≤ ENNReal.ofReal (2 * Real.exp (-(↑n * ε ^ 2 / 16))) / (uniformSphereMeasure n) A

theorem HighDimensional.isoperimetric_sphere_weak (n : ℕ) (ε : ℝ) (hε : 0 < ε) (A : Set (UnitSphere n)) (hA : (uniformSphereMeasure n) A ≠ 0) : (uniformSphereMeasure n) (Metric.thickening ε A)ᶜ ≤ ENNReal.ofReal (2 * Real.exp (-(↑n * ε ^ 2 / 16))) / (uniformSphereMeasure n) A

theorem HighDimensional.jl_probabilistic_method (d n : ℕ) (hn : 2 ≤ n) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) (S : Fin n → EuclideanSpace ℝ (Fin d)) (hd : 72 * ε⁻¹ ^ 2 * Real.log ↑n + 1 < ↑d) : ∃ (k : ℕ), ↑k ≤ 72 * ε⁻¹ ^ 2 * Real.log ↑n + 1 ∧ ∃ (f : EuclideanSpace ℝ (Fin d) →ₗ[ℝ] EuclideanSpace ℝ (Fin k)), ∀ (i j : Fin n), ‖S i - S j‖ ≤ ‖f (S i) - f (S j)‖ ∧ ‖f (S i) - f (S j)‖ ≤ (1 + ε) * ‖S i - S j‖

theorem HighDimensional.johnson_lindenstrauss (d n : ℕ) (hn : 2 ≤ n) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) (S : Fin n → EuclideanSpace ℝ (Fin d)) : ∃ (k : ℕ), ↑k ≤ 72 * ε⁻¹ ^ 2 * Real.log ↑n + 1 ∧ ∃ (f : EuclideanSpace ℝ (Fin d) →ₗ[ℝ] EuclideanSpace ℝ (Fin k)), ∀ (i j : Fin n), ‖S i - S j‖ ≤ ‖f (S i) - f (S j)‖ ∧ ‖f (S i) - f (S j)‖ ≤ (1 + ε) * ‖S i - S j‖

theorem HighDimensional.dvoretzky_theorem : ∃ c > 0, ∀ (n : ℕ), 2 ≤ n → ∀ (ε : ℝ), 0 < ε → ∀ (C : ConvexBody (EuclideanSpace ℝ (Fin n))), (∀ x ∈ ↑C, -x ∈ ↑C) → ∃ (k : ℕ) (S : Submodule ℝ (EuclideanSpace ℝ (Fin n))) (_ : Module.finrank ℝ ↥S = k) (T : ↥S ≃ₗ[ℝ] EuclideanSpace ℝ (Fin k)), Metric.closedBall 0 1 ⊆ ⇑T '' (Subtype.val ⁻¹' ↑C) ∧ ⇑T '' (Subtype.val ⁻¹' ↑C) ⊆ Metric.closedBall 0 (1 + ε) ∧ ↑k ≥ c * ε ^ 2 / Real.log (1 + ε⁻¹) * Real.log ↑n

def ChernoffHoeffding.IsBoundedUnitInterval {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : Prop

theorem ChernoffHoeffding.chernoff_bound_unit_interval {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (X : Fin n → Ω → ℝ) (hBound : ∀ (i : Fin n), IsBoundedUnitInterval (X i) μ) (hIndep : ProbabilityTheory.iIndepFun X μ) (ε : ℝ) (hε : 0 < ε) : ∃ c > 0, μ {ω : Ω | |∑ i : Fin n, X i ω - ∫ (ω' : Ω), ∑ i : Fin n, X i ω' ∂μ| ≥ ε * ∑ i : Fin n, X i ω} ≤ ENNReal.ofReal (2 * Real.exp (-c * ε ^ 2 * ∫ (ω' : Ω), ∑ i : Fin n, X i ω' ∂μ))