PhysicalPairEnergy.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.UniversalDictionary.pairOverlap line 13
lemma OAI.DilutedSpinGlass.UniversalDictionary.pairOverlap_bound line 18
lemma OAI.DilutedSpinGlass.UniversalDictionary.shapeCovariance_pair line 33
lemma OAI.DilutedSpinGlass.UniversalDictionary.integrable_overlap_square line 47

theorem OAI.DilutedSpinGlass.UniversalDictionary.shape_energy_bound line 61

Source documentation

Physical singleton covariance bound. The only tree assumptions here are positional: exactly one eligible second leaf, and an actual common fork. All root integrability obligations are discharged for the true reservoir.

theorem shape_energy_bound (hd : d < L+1) (hab : splitDepth S a b = d)
    (v : S.Internal) (hav : freshSplitDepth S v a = d) (hbv : freshSplitDepth S v b = d)
    (huniq : ∀ c, splitDepth S a c = d → c = b)
    (hm : Monotone m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last (L+1)) = 1) :
    (-gamma S m v) * (∫ z,
      rootConditionalEnergy T (fun i => prior i.1.1) (fun j => m j.succ) base old d (readVector read) z
        ∂fullRootLaw ξ μ ν rate score) ≤
      (m ⟨d+1,by omega⟩-m ⟨d,by omega⟩) +
      shapeCovariance ξ μ ν (siteLaw N) rate score S a T m base old read (pairSplitTest d) true
        (pairOverlap S a b read) := by
…

Mentions: OAI.DilutedSpinGlass.UniversalDictionary.prior, OAI.DilutedSpinGlass.UniversalDictionary.readVector, OAI.DilutedSpinGlass.fullRootLaw, OAI.DilutedSpinGlass.UniversalDictionary.shapeCovariance, OAI.DilutedSpinGlass.UniversalDictionary.pairSplitTest, OAI.DilutedSpinGlass.UniversalDictionary.pairOverlap