RootProjectionIntegrability.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_treeOverlap line 14
lemma OAI.DilutedSpinGlass.PrescribedTree.treeOverlap_eq_spatialProduct line 20
def OAI.DilutedSpinGlass.HeterogeneousMarks.rootSplitProjector line 42
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootProjectedTriple line 47
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.rootSplitProjector_bound line 72
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootProjectedTriple line 78
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootTargetError line 90
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootTargetError line 120
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootOldError line 139
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootOldError line 166
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_rootMatrixObservableHistory line 204
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_rootMatrixObservableHistory line 229
Source documentation
Ordinary integrability of the literal signed multileaf history at the actual variable-alphabet root. This does NOT take its absolute value in the concentration identity: the crude bound is used only to justify integration.
```
lemma integrable_rootMatrixObservableHistory (μ : Measure (FullRootState Y X I M))
    [IsFiniteMeasure μ] (hF : ∀ x, |F x|≤1) (hg : ∀ x, |g x|≤1) :
    Integrable (fun z : FullRootState Y X I M =>
      matrixObservableHistory R q (rootTower T Q m base old z) (grid L 0 L) cs S a
        (fun x => F (fun c => physical (rootArray z.2.2.1 z.2.2.2) L (x c)))
        (fun x => g (fun b => physical (rootArray z.2.2.1 z.2.2.2) L (S.pathAt b x)))) μ := by
…
```
Mentions: OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.HeterogeneousMarks.rootTower, OAI.DilutedSpinGlass.HeterogeneousMarks.physical, OAI.DilutedSpinGlass.rootArray