OAI/Probability/DilutedSpin/RootOverlapVariance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.FiniteLaw.mixedVariance line 10
2. lemma OAI.DilutedSpinGlass.FiniteLaw.mixedVariance_eq_centered line 14
3. lemma OAI.DilutedSpinGlass.FiniteLaw.mixedVariance_nonneg line 39
4. lemma OAI.DilutedSpinGlass.FiniteLaw.mixedVariance_le_one line 48
5. def OAI.DilutedSpinGlass.PrescribedTree.overlapVariance line 70
6. def OAI.DilutedSpinGlass.PrescribedTree.markerDefect line 76
7. theorem OAI.DilutedSpinGlass.PrescribedTree.overlapVariance_le_marker line 84

   Source documentation

   Root and prefix randomness are both retained. The square root is taken only after integrating the actual conditional energy.

   theorem overlapVariance_le_marker (μ : Measure Z) [IsProbabilityMeasure μ]
       (Ω : Z → Type) [∀ z, Fintype (Ω z)] (A : PrescribedTree n) (r : ℕ)
       (K : (z : Z) → KernelTower (Ω z) (n+1+r))
       (V : (z : Z) → FinitePath (Ω z) (n+1+r) → Fin N → ℝ)
       (hsq : Integrable (fun z => unarySquareMean A r (K z) (V z)) μ)
       (hpair : Integrable (fun z => forkPairMean A r (K z) (V z)) μ)
       (hE : Integrable (fun z => shapeEnergyAt A r (K z) (V z)) μ)
       (hEs : Integrable (fun z => Real.sqrt (shapeEnergyAt A r (K z) (V z))) μ) :
       overlapVariance μ Ω (stem (unary A) r) K V ≤
         Real.sqrt (∫ z, shapeEnergyAt A r (K z) (V z) ∂μ)+|markerDefect μ Ω A r K V| := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.unarySquareMean, OAI.DilutedSpinGlass.PrescribedTree.forkPairMean, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt, OAI.DilutedSpinGlass.PrescribedTree.overlapVariance, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.unary, OAI.DilutedSpinGlass.PrescribedTree.markerDefect

8. lemma OAI.DilutedSpinGlass.PrescribedTree.concrete_marker_covariance_eq_defect line 103