Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
production module

AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT

Read the mathematical statements and proofs in order

15 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean.

Imports
Mathlib.Probability.CentralLimitTheorem externalMathlib.MeasureTheory.Measure.Count externalMathlib.Algebra.BigOperators.Ring.Finset external
Imported by
AutoSamplingTheory.TechnicalLemmasAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropyTests.BalancedRademacherCLT
Placeholder scan
0 declaration(s) flagged
Gate status
Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.countLaw Partial Not mapped

No declaration docstring.

private def countLaw (α : Type*) [Fintype α] [MeasurableSpace α] : Measure α :=
  (Fintype.card α : ℝ≥0∞)⁻¹ • Measure.count

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:19published source at ed709a7f320d

instance AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.countLaw_probability Partial Not mapped

No declaration docstring.

private instance countLaw_probability (α : Type*) [Fintype α] [Nonempty α]
    [MeasurableSpace α] [MeasurableSingletonClass α] : IsProbabilityMeasure (countLaw α) := by
  constructor
  unfold countLaw
  simp only [Measure.smul_apply, smul_eq_mul]
  rw [Measure.count_apply_finite Set.univ Set.finite_univ]
  simp only [Set.Finite.toFinset_univ, Finset.card_univ]
  exact ENNReal.inv_mul_cancel (by exact_mod_cast Fintype.card_ne_zero)
    (by simp)

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:22published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.countLaw_integral Partial Not mapped

No declaration docstring.

private theorem countLaw_integral {α : Type*} [Fintype α] [MeasurableSpace α]
    [MeasurableSingletonClass α] {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E] (f : α → E) :
    (∫ a, f a ∂countLaw α) = (Fintype.card α : ℝ)⁻¹ • ∑ a : α, f a := by
  unfold countLaw
  rw [integral_smul_measure, integral_fintype (Integrable.of_finite : Integrable f Measure.count)]
  simp

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:32published source at ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.sign Partial Not mapped

No declaration docstring.

private def sign (b : Bool) : ℝ := if b then 1 else -1

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:40published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.sign_mean Partial Not mapped

No declaration docstring.

private theorem sign_mean : (∫ b, sign b ∂countLaw Bool) = 0 := by
  rw [countLaw_integral]
  norm_num [Fintype.sum_bool, sign]

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:42published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.sign_second_moment Partial Not mapped

No declaration docstring.

private theorem sign_second_moment : (∫ b, (sign b) ^ 2 ∂countLaw Bool) = 1 := by
  rw [countLaw_integral]
  norm_num [Fintype.sum_bool, sign]

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:46published source at ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.coordinateLaw Partial Not mapped

No declaration docstring.

private def coordinateLaw : Measure ℝ := (countLaw Bool).map sign

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:50published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.coordinate_charFun Partial Not mapped

No declaration docstring.

private theorem coordinate_charFun (t : ℝ) :
    charFun coordinateLaw t =
      (2 : ℂ)⁻¹ * ∑ b : Bool, Complex.exp ((t : ℂ) * (sign b : ℂ) * Complex.I) := by
  rw [coordinateLaw, charFun_apply_real,
    integral_map (measurable_of_countable sign).aemeasurable (by fun_prop),
    countLaw_integral]
  simp only [Fintype.card_bool, Nat.cast_ofNat, Complex.real_smul, Complex.ofReal_inv,
    Complex.ofReal_ofNat]

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:52published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.unscaled_charFun Partial Not mapped

No declaration docstring.

private theorem unscaled_charFun (n : ℕ) (t : ℝ) :
    charFun ((countLaw (Fin n → Bool)).map (fun ε => ∑ j : Fin n, sign (ε j))) t =
      (charFun coordinateLaw t) ^ n := by
  rw [charFun_apply_real,
    integral_map (measurable_of_countable _).aemeasurable (by fun_prop),
    countLaw_integral, coordinate_charFun]
  have hexp (ε : Fin n → Bool) :
      Complex.exp ((t : ℂ) * ((∑ j : Fin n, sign (ε j) : ℝ) : ℂ) * Complex.I) =
        ∏ j : Fin n, Complex.exp ((t : ℂ) * (sign (ε j) : ℂ) * Complex.I) := by
    rw [← Complex.exp_sum]
    congr 1
    simp only [Complex.ofReal_sum, Finset.mul_sum,
      Finset.sum_mul]
  simp_rw [hexp]
  rw [← Fintype.sum_pow
    (fun b : Bool => Complex.exp ((t : ℂ) * (sign b : ℂ) * Complex.I)) n]
  simp only [Fintype.card_fun, Fintype.card_fin, Fintype.card_bool, Nat.cast_pow,
    Nat.cast_ofNat, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_pow,
    Complex.ofReal_ofNat, inv_pow, mul_pow]

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:61published source at ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.normalizedSum Partial Not mapped

No declaration docstring.

private def normalizedSum (n : ℕ) (ε : Fin n → Bool) : ℝ :=
  (Real.sqrt (n : ℝ))⁻¹ * ∑ j : Fin n, sign (ε j)

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:81published source at ed709a7f320d

def AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.actualLaw Partial Not mapped

No declaration docstring.

private def actualLaw (n : ℕ) : ProbabilityMeasure ℝ :=
  ⟨(countLaw (Fin n → Bool)).map (normalizedSum n),
    (countLaw (Fin n → Bool)).isProbabilityMeasure_map
      (measurable_of_countable (normalizedSum n)).aemeasurable⟩

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:84published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.actualLaw_zero Partial Not mapped

No declaration docstring.

private theorem actualLaw_zero : (actualLaw 0 : Measure ℝ) = Measure.dirac 0 := by
  have hzero : normalizedSum 0 = fun _ => 0 := by
    funext ε
    simp [normalizedSum]
  change (countLaw (Fin 0 → Bool)).map (normalizedSum 0) = Measure.dirac 0
  rw [hzero]
  simp

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:89published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.normalized_charFun Partial Not mapped

No declaration docstring.

private theorem normalized_charFun (n : ℕ) (t : ℝ) :
    charFun (actualLaw n) t =
      (charFun coordinateLaw ((Real.sqrt (n : ℝ))⁻¹ * t)) ^ n := by
  change charFun ((countLaw (Fin n → Bool)).map
    (fun ε => (Real.sqrt (n : ℝ))⁻¹ * ∑ j : Fin n, sign (ε j))) t = _
  rw [charFun_map_mul_comp (measurable_of_countable _).aemeasurable]
  exact unscaled_charFun n _

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:97published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.actualLaw_tendsto Partial Not mapped

No declaration docstring.

private theorem actualLaw_tendsto :
    Tendsto actualLaw atTop
      (𝓝 (⟨gaussianReal 0 1, inferInstance⟩ : ProbabilityMeasure ℝ)) := by
  apply ProbabilityMeasure.tendsto_iff_tendsto_charFun.mpr
  intro t
  simp_rw [normalized_charFun]
  have hlim := tendsto_charFun_inv_sqrt_mul_pow
    (measurable_of_countable sign).aemeasurable sign_mean
    (by simpa only [Pi.pow_apply] using sign_second_moment) t
  simpa [coordinateLaw, charFun_gaussianReal, neg_div] using hlim

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:105published source at ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT.balanced_count_sum_tendsto_gaussian Partial Not mapped

Read the complete mathematical statement and proof, with Lean below each

No declaration docstring.

theorem balanced_count_sum_tendsto_gaussian :
    ∃ laws : ℕ → ProbabilityMeasure ℝ,
      (∀ n : ℕ, (laws n : Measure ℝ) =
        (((Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ •
          (Measure.count : Measure (Fin n → Bool))).map
          (fun ε : Fin n → Bool => (Real.sqrt (n : ℝ))⁻¹ *
            ∑ j : Fin n, if ε j then (1 : ℝ) else -1))) ∧
      (laws 0 : Measure ℝ) = Measure.dirac 0 ∧
      Tendsto (fun n : ℕ => laws (n + 1)) atTop
        (𝓝 (⟨gaussianReal 0 1, inferInstance⟩ : ProbabilityMeasure ℝ)) := by
  refine ⟨actualLaw, ?_, actualLaw_zero, ?_⟩
  · intro n
    rfl
  · exact actualLaw_tendsto.comp (tendsto_add_atTop_nat 1)

end AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean:116published source at ed709a7f320dOpen detailed card

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Probability/BalancedRademacherCLT.lean — full module with imports and context
Download module (.lean)
import Mathlib.Probability.CentralLimitTheorem
import Mathlib.MeasureTheory.Measure.Count
import Mathlib.Algebra.BigOperators.Ring.Finset

/-!
# Actual finite balanced-count normalized sums

The finite laws are literal normalized counting measures. The characteristic
function adapter below is authored for these laws; the scalar CLT and Levy
convergence are reused from the repository-pinned Mathlib. Weak convergence
alone provides no entropy, coordinate-energy, LSI, T2 or cost conclusion.
-/

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal BigOperators Topology
noncomputable section
namespace AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT

private def countLaw (α : Type*) [Fintype α] [MeasurableSpace α] : Measure α :=
  (Fintype.card α : ℝ≥0∞)⁻¹ • Measure.count

private instance countLaw_probability (α : Type*) [Fintype α] [Nonempty α]
    [MeasurableSpace α] [MeasurableSingletonClass α] : IsProbabilityMeasure (countLaw α) := by
  constructor
  unfold countLaw
  simp only [Measure.smul_apply, smul_eq_mul]
  rw [Measure.count_apply_finite Set.univ Set.finite_univ]
  simp only [Set.Finite.toFinset_univ, Finset.card_univ]
  exact ENNReal.inv_mul_cancel (by exact_mod_cast Fintype.card_ne_zero)
    (by simp)

private theorem countLaw_integral {α : Type*} [Fintype α] [MeasurableSpace α]
    [MeasurableSingletonClass α] {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E] (f : α → E) :
    (∫ a, f a ∂countLaw α) = (Fintype.card α : ℝ)⁻¹ • ∑ a : α, f a := by
  unfold countLaw
  rw [integral_smul_measure, integral_fintype (Integrable.of_finite : Integrable f Measure.count)]
  simp

private def sign (b : Bool) : ℝ := if b then 1 else -1

private theorem sign_mean : (∫ b, sign b ∂countLaw Bool) = 0 := by
  rw [countLaw_integral]
  norm_num [Fintype.sum_bool, sign]

private theorem sign_second_moment : (∫ b, (sign b) ^ 2 ∂countLaw Bool) = 1 := by
  rw [countLaw_integral]
  norm_num [Fintype.sum_bool, sign]

private def coordinateLaw : Measure ℝ := (countLaw Bool).map sign

private theorem coordinate_charFun (t : ℝ) :
    charFun coordinateLaw t =
      (2 : ℂ)⁻¹ * ∑ b : Bool, Complex.exp ((t : ℂ) * (sign b : ℂ) * Complex.I) := by
  rw [coordinateLaw, charFun_apply_real,
    integral_map (measurable_of_countable sign).aemeasurable (by fun_prop),
    countLaw_integral]
  simp only [Fintype.card_bool, Nat.cast_ofNat, Complex.real_smul, Complex.ofReal_inv,
    Complex.ofReal_ofNat]

private theorem unscaled_charFun (n : ℕ) (t : ℝ) :
    charFun ((countLaw (Fin n → Bool)).map (fun ε => ∑ j : Fin n, sign (ε j))) t =
      (charFun coordinateLaw t) ^ n := by
  rw [charFun_apply_real,
    integral_map (measurable_of_countable _).aemeasurable (by fun_prop),
    countLaw_integral, coordinate_charFun]
  have hexp (ε : Fin n → Bool) :
      Complex.exp ((t : ℂ) * ((∑ j : Fin n, sign (ε j) : ℝ) : ℂ) * Complex.I) =
        ∏ j : Fin n, Complex.exp ((t : ℂ) * (sign (ε j) : ℂ) * Complex.I) := by
    rw [← Complex.exp_sum]
    congr 1
    simp only [Complex.ofReal_sum, Finset.mul_sum,
      Finset.sum_mul]
  simp_rw [hexp]
  rw [← Fintype.sum_pow
    (fun b : Bool => Complex.exp ((t : ℂ) * (sign b : ℂ) * Complex.I)) n]
  simp only [Fintype.card_fun, Fintype.card_fin, Fintype.card_bool, Nat.cast_pow,
    Nat.cast_ofNat, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_pow,
    Complex.ofReal_ofNat, inv_pow, mul_pow]

private def normalizedSum (n : ℕ) (ε : Fin n → Bool) : ℝ :=
  (Real.sqrt (n : ℝ))⁻¹ * ∑ j : Fin n, sign (ε j)

private def actualLaw (n : ℕ) : ProbabilityMeasure ℝ :=
  ⟨(countLaw (Fin n → Bool)).map (normalizedSum n),
    (countLaw (Fin n → Bool)).isProbabilityMeasure_map
      (measurable_of_countable (normalizedSum n)).aemeasurable⟩

private theorem actualLaw_zero : (actualLaw 0 : Measure ℝ) = Measure.dirac 0 := by
  have hzero : normalizedSum 0 = fun _ => 0 := by
    funext ε
    simp [normalizedSum]
  change (countLaw (Fin 0 → Bool)).map (normalizedSum 0) = Measure.dirac 0
  rw [hzero]
  simp

private theorem normalized_charFun (n : ℕ) (t : ℝ) :
    charFun (actualLaw n) t =
      (charFun coordinateLaw ((Real.sqrt (n : ℝ))⁻¹ * t)) ^ n := by
  change charFun ((countLaw (Fin n → Bool)).map
    (fun ε => (Real.sqrt (n : ℝ))⁻¹ * ∑ j : Fin n, sign (ε j))) t = _
  rw [charFun_map_mul_comp (measurable_of_countable _).aemeasurable]
  exact unscaled_charFun n _

private theorem actualLaw_tendsto :
    Tendsto actualLaw atTop
      (𝓝 (⟨gaussianReal 0 1, inferInstance⟩ : ProbabilityMeasure ℝ)) := by
  apply ProbabilityMeasure.tendsto_iff_tendsto_charFun.mpr
  intro t
  simp_rw [normalized_charFun]
  have hlim := tendsto_charFun_inv_sqrt_mul_pow
    (measurable_of_countable sign).aemeasurable sign_mean
    (by simpa only [Pi.pow_apply] using sign_second_moment) t
  simpa [coordinateLaw, charFun_gaussianReal, neg_div] using hlim

theorem balanced_count_sum_tendsto_gaussian :
    ∃ laws : ℕ → ProbabilityMeasure ℝ,
      (∀ n : ℕ, (laws n : Measure ℝ) =
        (((Fintype.card (Fin n → Bool) : ℝ≥0∞)⁻¹ •
          (Measure.count : Measure (Fin n → Bool))).map
          (fun ε : Fin n → Bool => (Real.sqrt (n : ℝ))⁻¹ *
            ∑ j : Fin n, if ε j then (1 : ℝ) else -1))) ∧
      (laws 0 : Measure ℝ) = Measure.dirac 0 ∧
      Tendsto (fun n : ℕ => laws (n + 1)) atTop
        (𝓝 (⟨gaussianReal 0 1, inferInstance⟩ : ProbabilityMeasure ℝ)) := by
  refine ⟨actualLaw, ?_, actualLaw_zero, ?_⟩
  · intro n
    rfl
  · exact actualLaw_tendsto.comp (tendsto_add_atTop_nat 1)

end AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT