NSpinVariance.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The Haar contribution to the enriched pressure variance.

lemma OAI.InvariantIsing.integral_sq_sub_le_of_gaussian_tail line 17

Source documentation

Integrating the Gaussian tail of a deviation gives its second moment. The proof applies layer cake to the squared deviation, so only the elementary exponential integral on the positive half-line is needed.

lemma integral_sq_sub_le_of_gaussian_tail {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (f : Ω → ℝ) (hf : Measurable f)
    (m C a : ℝ) (hC : 0 ≤ C) (ha : 0 < a)
    (htail : ∀ r : ℝ, 0 < r →
      μ.real {ω | r ≤ |f ω - m|} ≤ C * Real.exp (-a * r ^ 2)) :
    Integrable (fun ω => (f ω - m) ^ 2) μ ∧
      (∫ ω, (f ω - m) ^ 2 ∂μ) ≤ C / a := by
…

lemma OAI.InvariantIsing.variance_le_of_gaussian_median_tail line 57

theorem OAI.InvariantIsing.haar_enrichedPressure_variance line 69

Source documentation

Haar variance of the actual enriched pressure is at most a universal constant times the squared spectral bound divided by dimension.

theorem haar_enrichedPressure_variance (hpub : HaarConcentrationInput) :
    ∃ C : ℝ, 0 < C ∧
    ∀ N : ℕ, 3 ≤ N →
    ∀ μ : Measure (SpecialOrthogonal N),
      IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
    ∀ n : ℕ, ∀ b : ℕ → ℝ, ∀ v : ℕ → ℝ≥0, ∀ root : ℝ≥0,
      IsingPerceptron.CascadeExponents n b →
    ∀ eig c : Fin N → ℝ, ∀ K : ℝ, 0 < K → (∀ i, |eig i| ≤ K) →
      variance (fun U : SpecialOrthogonal N =>
        rotatedEnrichedPressure n b v root eig (specialRotation U) c) μ ≤
        C * K ^ 2 / N := by
…

Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.IsingPerceptron.CascadeExponents, OAI.InvariantIsing.rotatedEnrichedPressure, OAI.InvariantIsing.specialRotation