OAI/Probability/InvariantIsing/Spectral/SpectralQuantileMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.finite_sum_square_eq line 14
2. lemma OAI.InvariantIsing.integrable_finite_sum_square line 19
3. lemma OAI.InvariantIsing.integral_finite_sum_square line 26
4. lemma OAI.InvariantIsing.ae_sum_zero_of_pair_moments line 36

   Source documentation

   Pair moments alone preserve every finite linear relation. This avoids assuming a simultaneous vector law before it has been constructed.

   lemma ae_sum_zero_of_pair_moments {Ω T ι : Type*}
       [MeasurableSpace Ω] [MeasurableSpace T] [Fintype ι]
       {μ : Measure Ω} {ν : Measure T} {f : ι → Ω → ℝ} {g : ι → T → ℝ}
       (hf : ∀ i j, Integrable (fun x => f i x * f j x) μ)
       (hg : ∀ i j, Integrable (fun x => g i x * g j x) ν)
       (he : ∀ i j, (∫ x, f i x * f j x ∂μ) = ∫ x, g i x * g j x ∂ν)
       (hz : ∀ᵐ x ∂ν, (∑ i, g i x) = 0) :
       ∀ᵐ x ∂μ, (∑ i, f i x) = 0 := by
   …

5. lemma OAI.InvariantIsing.integral_scaled_product line 57
6. theorem OAI.InvariantIsing.spectralQuantilePath_linear_relation line 66

   Source documentation

   Every linear relation among nonnegative spectral combinations holds almost everywhere for their common quantile parameter.

   theorem spectralQuantilePath_linear_relation {m k : ℕ}
       {Q : ProbabilityMeasure (SpectralArray m)}
       (hgg : HasEntryGhirlandaGuerra (fun x i j => x (i,j)) (Q : Measure (SpectralArray m)))
       (hG : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), SpectralGram x)
       (q : Fin m → ℝ) (hq : ∀ a, 0 ≤ q a)
       (hd : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), ∀ i a, (x (i,i) a : ℝ) = q a)
       (hE : ∀ e : Equiv.Perm ℕ,
         (Q : Measure (SpectralArray m)).map (permuteSpectralArray e) = Q)
       (w : Fin k → Fin m → ℝ) (hw : ∀ i a, 0 ≤ w i a)
       (hs : ∀ i, ∀ᵐ x ∂(Q : Measure (SpectralArray m)),
         spectralLinearArray (w i) x 0 1 ∈ Icc (0 : ℝ) 1)
       (c : Fin k → ℝ) (hc : ∀ a, (∑ i, c i * w i a) = 0) :
   …

   Mentions: OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.SpectralGram, OAI.InvariantIsing.permuteSpectralArray, OAI.InvariantIsing.spectralLinearArray