OAI/Probability/DilutedSpin/QTopologyBound.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.insertionRadius line 10
2. def OAI.DilutedSpinGlass.normalizedInsertion line 11
3. lemma OAI.DilutedSpinGlass.insertionRadius_pos line 14
4. lemma OAI.DilutedSpinGlass.insertionRadius_lt_one line 19
5. lemma OAI.DilutedSpinGlass.normalizedInsertion_bound line 24
6. lemma OAI.DilutedSpinGlass.normalizedInsertion_log line 34
7. lemma OAI.DilutedSpinGlass.KernelTower.backwardLog_normalized line 44
8. lemma OAI.DilutedSpinGlass.PrescribedTree.chargeBound_mono line 68
9. def OAI.DilutedSpinGlass.PrescribedTree.qMass line 80
10. lemma OAI.DilutedSpinGlass.PrescribedTree.qMass_nonneg line 83
11. def OAI.DilutedSpinGlass.PrescribedTree.shapeCharge line 89

    Source documentation

    A shape-only constant, independent of every assigned depth and system size.

    noncomputable def shapeCharge (k : ℕ) (S : ReducedTopology) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.ReducedTopology

12. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeCharge_nonneg line 92
13. lemma OAI.DilutedSpinGlass.PrescribedTree.qMass_realize_le line 95
14. lemma OAI.DilutedSpinGlass.PrescribedTree.bounded_terminal_majorant line 124

    Source documentation

    Finite enumeration is an inequality, not a quotient: multiple schedules representing the same tree can only increase this nonnegative majorant.

    lemma bounded_terminal_majorant {L K : ℕ} (F : PrescribedTree L → ℝ)
        (hF : ∀ T, 0 ≤ F T) (T : PrescribedTree L) (hT : T.leaves ≤ K) :
        F T ≤ ∑ S∈ReducedTopology.boundedTopologies K,
          ∑ q : S.Vertex → Fin L, if S.Admissible (fun v => q v) 0 L then
            (if T=S.realize L 0 (fun v => q v) then F (S.realize L 0 (fun v => q v)) else 0) else 0 := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.ReducedTopology.boundedTopologies, OAI.DilutedSpinGlass.q

15. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_bounded_majorant line 138