OAI/Probability/InvariantIsing/Arrays/NSpinConcentration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.measurable_rotatedFieldTerminal_joint line 14
2. lemma OAI.InvariantIsing.measurable_rotatedCascadeValue_joint line 29
3. lemma OAI.InvariantIsing.measurable_rotatedEnrichedPressure line 42
4. theorem OAI.InvariantIsing.haar_enrichedPressure_median_tail line 50

   Source documentation

   Uniform Haar tails for the finite enriched Ising pressure, conditional only on the precise published concentration input.

   theorem haar_enrichedPressure_median_tail (hpub : HaarConcentrationInput) :
       ∃ C c₀ : ℝ, 0 < 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) →
       ∃ m : ℝ,
         (1 / 2 : ℝ) ≤ μ.real {U | rotatedEnrichedPressure n b v root eig (specialRotation U) c ≤ m} ∧
         (1 / 2 : ℝ) ≤ μ.real {U | m ≤ rotatedEnrichedPressure n b v root eig (specialRotation U) c} ∧
         ∀ r : ℝ, 0 < r →
   …

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