OAI/Probability/DilutedSpin/TerminalInterior.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.FiniteLaw.exists_weight_pos line 10
2. lemma OAI.DilutedSpinGlass.FiniteLaw.tilt_weight_pos line 17
3. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_lt_const line 21
4. lemma OAI.DilutedSpinGlass.FiniteLaw.spinMean_interior line 31
5. lemma OAI.DilutedSpinGlass.FiniteLaw.bind_tilt_spinMean_interior line 42
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.terminalInterior_tilted line 62

   Source documentation

   Finite physical full support survives every old marked factor and every sequential tilt, even when the auxiliary priors have zero masses.

   lemma terminalInterior_tilted (r : ℕ) {k : ℕ} (roots : Fin k → I)
       (P : FiniteLaw Ω) (a : Ω) (Q : (i : I) → Fin (r+1) → FiniteLaw (A i))
       (m : Fin (r+1) → ℝ) (f : FinitePath (Ω×Row roots) (r+1) → ℝ)
       (s : Ω → ℝ) (hs : ∀ x, |s x|≤1)
       (hl : ∃ x, 0<P.weight x ∧ s x<1) (hu : ∃ x, 0<P.weight x ∧ -1<s x) :
       TerminalInterior r (tilt (r+1) (tower roots (r+1) (terminalTower a P r) Q) m f)
         (fun y => s (terminalState r (physical roots (r+1) y))) := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.Row, OAI.DilutedSpinGlass.HeterogeneousMarks.tower, OAI.DilutedSpinGlass.HeterogeneousMarks.physical