OAI/Probability/DilutedSpin/MeasurableProjectionError.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.measurable_dot line 13
2. lemma OAI.DilutedSpinGlass.FiniteLaw.l2_le_two line 18
3. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_tailMean_tilt line 30
4. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_splitProjector_tilt line 41
5. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_matrixProjectionError_tilt line 53
6. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_oldProjectionError_tilt line 65
7. lemma OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_le_two line 78
8. lemma OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError_le_two line 88
9. lemma OAI.DilutedSpinGlass.KernelTower.measurable_tripleExpectAt_tilt line 102
10. lemma OAI.DilutedSpinGlass.KernelTower.abs_tripleExpectAt_le line 122
11. lemma OAI.DilutedSpinGlass.KernelTower.measurable_halfTripleDifferenceAt_tilt line 134
12. lemma OAI.DilutedSpinGlass.KernelTower.abs_halfTripleDifferenceAt_le_two line 142
13. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_labeledHistory line 170
14. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_matrixObservableHistory_tilt line 187
15. lemma OAI.DilutedSpinGlass.PrescribedTree.matrixObservableHistory_bound line 207

    Source documentation

    A crude finite mass bound used ONLY for integrability. It is not a replacement for the signed centered covariance or the depth charging bound.

    lemma matrixObservableHistory_bound (K : KernelTower Ω L) (T S : PrescribedTree L)
        (q : C → T.Leaf) (cs : List C) (a : S.Leaf)
        (A : (C → FinitePath Ω L) → ℝ) (g : Sample Ω S → ℝ)
        (hA : ∀ x, |A x|≤1) (hg : ∀ x, |g x|≤1) :
        |matrixObservableHistory T q K (grid L 0 L) cs S a A g|≤
          historyMass (fun _ => 1) cs.length S ((Finset.univ.erase a).card) := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.matrixObservableHistory, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.historyMass