OAI/Probability/InvariantIsing/Arrays/NSpinTensorHaarFluctuation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.tensorRootTreeLaw line 16

   Source documentation

   Independent common Gaussian root and marked cascade.

   def tensorRootTreeLaw {N m k : ℕ} (I : Fin m → Finset (Fin N))
       (degree : Fin k → Fin m → ℕ) (n : ℕ) (b : ℕ → ℝ)
       (v : ℕ → SpinTensorIndex I degree → ℝ≥0) (root : SpinTensorIndex I degree → ℝ≥0) :
       Measure ((SpinTensorIndex I degree → ℝ) × NoiseTree (SpinTensorIndex I degree → ℝ) n) :=
   …

   Mentions: OAI.InvariantIsing.SpinTensorIndex

2. instance OAI.InvariantIsing.tensorRootTreeLaw_probability line 23
3. def OAI.InvariantIsing.tensorDisorderPressure line 34

   Source documentation

   The normalized spin/leaf log partition retaining all three disorders.

   def tensorDisorderPressure {N m k : ℕ} (eig c : Fin N → ℝ)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ) (n : ℕ)
       (p : SpecialOrthogonal N × ((SpinTensorIndex I degree → ℝ) ×
         NoiseTree (SpinTensorIndex I degree → ℝ) n)) : ℝ :=
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.SpinTensorIndex

4. lemma OAI.InvariantIsing.measurable_tensorLeafState line 40
5. lemma OAI.InvariantIsing.measurable_tensorDisorderPressure line 49
6. lemma OAI.InvariantIsing.tensorDisorderPressure_conditional_mean line 68
7. theorem OAI.InvariantIsing.tensorDisorderPressure_variance line 91

   Source documentation

   The full pressure variance is the sum of the root/cascade conditional contribution and the Haar variance of its conditional mean.

   theorem tensorDisorderPressure_variance (hhaar : HaarConcentrationInput)
       (hgauss : GaussianLipschitzVarianceInput) :
       ∃ C : ℝ, 0 < C ∧
       ∀ N : ℕ, 3 ≤ N →
       ∀ μ : Measure (SpecialOrthogonal N), IsProbabilityMeasure μ → μ.IsMulLeftInvariant →
       ∀ m k : ℕ, ∀ eig c : Fin N → ℝ, ∀ K : ℝ, 0 < K → (∀ i, |eig i| ≤ K) →
       ∀ I : Fin m → Finset (Fin N), ∀ degree : Fin k → Fin m → ℕ,
       ∀ amplitude : Fin k → ℝ, ∀ n : ℕ, ∀ b : ℕ → ℝ, CascadeExponents n b →
       ∀ site : ℕ → ℝ≥0, ∀ monomial : ℕ → Fin k → ℝ≥0,
         let v := fun i => tensorVarianceProfile I degree (site i) (monomial i)
   …

   Mentions: OAI.InvariantIsing.HaarConcentrationInput, OAI.InvariantIsing.GaussianLipschitzVarianceInput, OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.tensorVarianceProfile