OAI/Probability/DilutedSpin/RegularNodeEstimates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DilutedSpinGlass.UniversalDictionary.physicalChildMass line 17

    Source documentation

    The old or genuinely delayed proper-child projection cost, in the same physical scheduled covariance family as the parent.

    noncomputable def physicalChildMass (M : Model p) (θB hB : ℝ) (N L : ℕ)
    (u : Spec L × ℕ → ℝ) (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
    (s : Bool) (Q : Option (ReducedTopology.node k hk C).Vertex → Fin (L+1)) : ℝ :=
…

    Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.ReducedTopology

  2. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalChildMass_nonneg line 24
  3. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalChildMass_le_square line 31
  4. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalChildMass_le_sqrt line 45
  5. def OAI.DilutedSpinGlass.UniversalDictionary.physicalNodeShift line 57
  6. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalNodeShift_nonneg line 69
  7. def OAI.DilutedSpinGlass.UniversalDictionary.nodeShiftBudget line 76

    Source documentation

    Topology-dependent quadratic energy budget in the depth continuity bound.

    noncomputable def nodeShiftBudget (k : ℕ+) (C : Fin k → ReducedTopology) : ℝ :=
…

    Mentions: OAI.DilutedSpinGlass.ReducedTopology

  8. lemma OAI.DilutedSpinGlass.UniversalDictionary.nodeShiftBudget_nonneg line 80
  9. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalNodeShift_average line 83
  10. lemma OAI.DilutedSpinGlass.UniversalDictionary.multileaf_scalar_bound line 90
  11. def OAI.DilutedSpinGlass.BoundedDistance line 113

    Source documentation

    A bounded-test distance, with the scale written outside the test.

    def BoundedDistance (μ ν : Measure X) (d : ℝ) : Prop :=
…
  12. lemma OAI.DilutedSpinGlass.BoundedDistance.symm line 117
  13. lemma OAI.DilutedSpinGlass.BoundedDistance.prod line 123
  14. lemma OAI.DilutedSpinGlass.BoundedDistance.prod_left line 134
  15. lemma OAI.DilutedSpinGlass.poisson_boundedDistance line 145
  16. lemma OAI.DilutedSpinGlass.BoundedDistance.familyLaw line 151
  17. lemma OAI.DilutedSpinGlass.fullRoot_boundedDistance line 167