OAI/Probability/DilutedSpin/PhysicalOverlapConcentration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.markerMatrixCovariance_uncast line 13
2. def OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapVariance line 33
3. def OAI.DilutedSpinGlass.UniversalDictionary.physicalMarkerDefect line 44
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl.markerDefect line 56
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalOverlapVariance_le_marker line 107
6. lemma OAI.DilutedSpinGlass.DepthAverage.average_domain_bound line 130
7. lemma OAI.DilutedSpinGlass.DepthAverage.average_option_interval_bound line 143
8. theorem OAI.DilutedSpinGlass.ReducedTopology.regular_overlap_average_bound line 181

   Source documentation

   A positive fraction of early marker prefixes transfers the covariance estimate without a mesh-size penalty or a diagonal depth restriction.

   theorem regular_overlap_average_bound (S : ReducedTopology) {η : ℝ}
       (hη : 0<η) (hη1 : η≤1) (hlarge : 8<η*(L:ℝ))
       (F : (S.Vertex → Fin L) → ℝ) (E D : (Option S.Vertex → Fin L) → ℝ)
       (hF : ∀ q, 0≤F q) (hE : ∀ Q, 0≤E Q) (hD : ∀ Q, 0≤D Q)
       (hpoint : ∀ Q, regularShapeDomain S L (η/8) Q →
         F (fun v => Q (some v))≤Real.sqrt (E Q)+D Q) :
       (η/8)*average (regularOverlapDomain S L η) F ≤
         Real.sqrt (average (regularShapeDomain S L (η/8)) E)+
         average (regularShapeDomain S L (η/8)) D := by
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.regularShapeDomain, OAI.DilutedSpinGlass.ReducedTopology.regularOverlapDomain