OAI/Probability/InvariantIsing/Spectral/SpectralGG.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.spectralMonomial_self_deviation_le line 15
2. def OAI.InvariantIsing.spectralPerturbationCoefficients line 34

   Source documentation

   The concrete Haar-dependent tensor coefficient map.

   def spectralPerturbationCoefficients {Ω : Type*} {N m : ℕ}
       (U : Ω → SpecialOrthogonal N) (I : Fin m → Finset (Fin N))
       (d : Fin m → ℕ) (n r : ℕ) : Ω → (Spin N × LabeledLeaf n) → ℕ →₀ ℝ :=
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin

3. def OAI.InvariantIsing.spectralPerturbationKernel line 39
4. lemma OAI.InvariantIsing.spectralPerturbationCoefficients_cross line 45
5. lemma OAI.InvariantIsing.measurable_spectralPerturbationFields line 53
6. lemma OAI.InvariantIsing.measurable_spectralPerturbationCross line 64
7. theorem OAI.InvariantIsing.spectralPerturbation_gg_bound line 79

   Source documentation

   Concrete conditional Gaussian GG estimate. The distribution of the external rotation and the other disorder is arbitrary; Gaussian coordinates are the independent product factor.

   theorem spectralPerturbation_gg_bound {Ω : Type*} [MeasurableSpace Ω]
       {P : Measure Ω} [IsProbabilityMeasure P] {N m n k : ℕ}
       (U : Ω → SpecialOrthogonal N) (hU : Measurable U)
       (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ) (treeDegree : ℕ)
       {ν : Ω → Measure (Spin N × LabeledLeaf n)} (hν : Measurable ν)
       [∀ ω, IsProbabilityMeasure (ν ω)] (t b d₀ : ℝ)
       (D : Ω → (Fin (k + 1) → Spin N × LabeledLeaf n) → ℝ)
       (hDm : Measurable (Function.uncurry D)) {c : ℝ} (hc : 0 ≤ c)
       (hD : ∀ ω σ, |D ω σ| ≤ c)
       (hE : Integrable (fun z : Ω × (ℕ → ℝ) => ∫ x,
         |cylinderField (spectralPerturbationCoefficients U I d n treeDegree z.1 x) z.2 - b|
           ∂(ν z.1).tilted (fun x => t *
   …

   Mentions: OAI.InvariantIsing.SpecialOrthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spectralPerturbationCoefficients