OAI/Probability/DilutedSpin/RealEncoding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.mapModel line 12
2. lemma OAI.DilutedSpinGlass.mapModel_interaction_integrable line 20
3. lemma OAI.DilutedSpinGlass.mapModel_field_integrable line 28
4. lemma OAI.DilutedSpinGlass.integral_pi_map line 36
5. lemma OAI.DilutedSpinGlass.indexAverage_mapModel line 46
6. lemma OAI.DilutedSpinGlass.pressure_mapModel line 54
7. lemma OAI.DilutedSpinGlass.logMean_add_constant line 83
8. lemma OAI.DilutedSpinGlass.trialLog_add_constant line 94
9. lemma OAI.DilutedSpinGlass.FiniteLaw.asProbability_map line 117
10. def OAI.DilutedSpinGlass.KernelTower.realEncode line 133

    Source documentation

    Literal messages at leaves, with no spin terminal transition.

    noncomputable def realEncode : (r : ℕ) → KernelTower Ω r →
        (FinitePath Ω r → ℝ) → Hierarchy r
      | 0,_,V => V ()
      | r+1,T,V => T.1.asProbability (fun a => realEncode r (T.2 a) (fun y => V (a,y)))
    
    /-- Pad a finite conditional law along an injection with a specified retraction.
    Off-support children are harmless but are specified, rather than postulated. -/

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Hierarchy, OAI.DilutedSpinGlass.KernelTower.law

11. def OAI.DilutedSpinGlass.KernelTower.embed line 140

    Source documentation

    Pad a finite conditional law along an injection with a specified retraction. Off-support children are harmless but are specified, rather than postulated.

    noncomputable def embed (f : Ω → Λ) (g : Λ → Ω) : (r : ℕ) →
        KernelTower Ω r → KernelTower Λ r
      | 0,_ => ()
      | r+1,T => (T.1.map f, fun a => embed f g r (T.2 (g a)))

    Mentions: OAI.DilutedSpinGlass.KernelTower

12. lemma OAI.DilutedSpinGlass.KernelTower.realEncode_embed line 145
13. lemma OAI.DilutedSpinGlass.KernelTower.backwardLog_realEncode line 166
14. lemma OAI.DilutedSpinGlass.finiteHierarchy_realization line 199

    Source documentation

    Every genuinely finitely branching measure hierarchy has a finite alphabet realization. Padding changes no law; in particular this imposes no restriction on the original variational class after density.

    lemma finiteHierarchy_realization (r : ℕ) (ζ : Hierarchy r) (hζ : FiniteHierarchy r ζ) :
        ∃ (n : ℕ) (_hn : 0 < n) (T : KernelTower (Fin n) r) (V : FinitePath (Fin n) r → ℝ),
          KernelTower.realEncode r T V = ζ := by
    …

    Mentions: OAI.DilutedSpinGlass.Hierarchy, OAI.DilutedSpinGlass.FiniteHierarchy, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.realEncode