theorem Concentration.chernoff_bound {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (X : Fin n → Ω → ℝ) (hIndep : ProbabilityTheory.iIndepFun X μ) (hRange : ∀ (i : Fin n) (ω : Ω), X i ω = 0 ∨ X i ω = 1) (p : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) (hProb : ∀ (i : Fin n), μ.real {ω : Ω | X i ω = 1} = p) (ε : ℝ) (hε : 0 ≤ ε) : μ.real {ω : Ω | |∑ i : Fin n, X i ω - ↑n * p| ≥ ε * (↑n * p)} ≤ 2 * Real.exp (-(↑n * p * ε ^ 2 / 12))

theorem Concentration.hoeffding_bound {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (X : Fin n → Ω → ℝ) (a : Fin n → ℝ) (hIndep : ProbabilityTheory.iIndepFun X μ) (hRange : ∀ (i : Fin n) (ω : Ω), X i ω = 1 ∨ X i ω = -1) (hProb : ∀ (i : Fin n), μ.real {ω : Ω | X i ω = 1} = 1 / 2) (ha : ∑ i : Fin n, a i ^ 2 = 1) (t : ℝ) (ht : 0 < t) : μ.real {ω : Ω | |∑ i : Fin n, a i * X i ω| > t} ≤ 2 * Real.exp (-t ^ 2 / 2)

theorem Concentration.inner_product_eq_dist_hyperplane {n : ℕ} (a x : EuclideanSpace ℝ (Fin n)) (ha : ‖a‖ = 1) : Metric.infDist x {y : EuclideanSpace ℝ (Fin n) | inner ℝ a y = 0} = |inner ℝ a x|

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

theorem VolumeHardness.convexHull_subset_iUnion_closedBalls {n m : ℕ} (hm : 0 < m) (P : Fin m → Fin n → ℝ) (hP : ∀ (i : Fin m), ‖P i‖ ≤ 1) : (convexHull ℝ) (Set.range P) ⊆ ⋃ (i : Fin m), Metric.closedBall (2⁻¹ • P i) 2⁻¹

theorem VolumeHardness.volume_convex_hull_points_bound (n : ℕ) (hn : 0 < n) (m : ℕ) (hm : 0 < m) (P : Fin m → Fin n → ℝ) (hP : ∀ (i : Fin m), ‖P i‖ ≤ 1) : MeasureTheory.Measure.addHaar ((convexHull ℝ) (Set.range P)) ≤ ENNReal.ofReal (↑m / 2 ^ n) * MeasureTheory.Measure.addHaar (Metric.ball 0 1)

theorem VolumeHardness.volume_computation_hardness (n : ℕ) (hn : 0 < n) (m : ℕ) (hm : 0 < m) (P : Fin m → Fin n → ℝ) (hP : ∀ (i : Fin m), ‖P i‖ ≤ 1) : MeasureTheory.Measure.addHaar (Metric.ball 0 1) ≥ ENNReal.ofReal (2 ^ n / ↑m) * MeasureTheory.Measure.addHaar ((convexHull ℝ) (Set.range P))