OAI/Probability/DilutedSpin/HeterogeneousMarks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DilutedSpinGlass.HeterogeneousMarks.Row line 15

   Source documentation

   The independent auxiliary mark row for the actually realized type list.

   abbrev Row {k : ℕ} (roots : Fin k → I) := (j : Fin k) → A (roots j)

2. def OAI.DilutedSpinGlass.HeterogeneousMarks.tower line 18

   Source documentation

   A product-prior tower on the physical state and all realized marks.

   noncomputable def tower {k : ℕ} (roots : Fin k → I) : (L : ℕ) →
       KernelTower Ω L → ((i : I) → Fin L → FiniteLaw (A i)) →
       KernelTower (Ω × Row (A := A) roots) L
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.HeterogeneousMarks.Row

3. def OAI.DilutedSpinGlass.HeterogeneousMarks.physical line 26

   Source documentation

   Forget all auxiliary marks.

   def physical {k : ℕ} (roots : Fin k → I) : (L : ℕ) →
       FinitePath (Ω × Row (A := A) roots) L → FinitePath Ω L
   …

   Mentions: OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.Row

4. def OAI.DilutedSpinGlass.HeterogeneousMarks.mark line 32

   Source documentation

   The path of the q-th realized mark, in that mark's own finite space.

   def mark {k : ℕ} {roots : Fin k → I} (q : Fin k) : (L : ℕ) →
       FinitePath (Ω × Row (A := A) roots) L → FinitePath (A (roots q)) L
   …

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.Row

5. def OAI.DilutedSpinGlass.HeterogeneousMarks.split line 38

   Source documentation

   Move one distinguished mark out of the dependent row.

   def split {k : ℕ} (roots : Fin k → I) (i : I) :
       (Ω × Row (A := A) (Fin.cons i roots)) ≃ ((Ω × Row (A := A) roots) × A i) where
   …

   Mentions: OAI.DilutedSpinGlass.HeterogeneousMarks.Row

6. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.tower_split line 48

   Source documentation

   Adding a type uses its own prior, independently of all old marks.

   theorem tower_split {k : ℕ} (roots : Fin k → I) (i : I) (L : ℕ)
       (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) :
       KernelTower.transport (split roots i) L (tower (Fin.cons i roots) L T Q) =
         KernelTower.prod L (tower roots L T Q) (markPrior L (Q i)) := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.KernelTower.transport, OAI.DilutedSpinGlass.HeterogeneousMarks.split, OAI.DilutedSpinGlass.HeterogeneousMarks.tower, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.markPrior

7. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.physical_split line 71
8. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.mark_split_succ line 84
9. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.mark_split_zero line 97
10. def OAI.DilutedSpinGlass.HeterogeneousMarks.logWeight line 111

    Source documentation

    A finite realized row in the full countable-type model.

    noncomputable def logWeight (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (y : FinitePath (Ω × Row (A := A) roots) L) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.Row

11. def OAI.DilutedSpinGlass.HeterogeneousMarks.insertedLog line 117

    Source documentation

    The insertion keeps the complete original mark row in the base law.

    noncomputable def insertedLog (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) (i : I)
        (y : FinitePath ((Ω × Row (A := A) roots) × A i) L) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.Row

12. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.insertedLog_split line 124
13. def OAI.DilutedSpinGlass.HeterogeneousMarks.root line 140

    Source documentation

    The quenched logarithmic root energy in the actual dependent mark row.

    noncomputable def root (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath

14. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_cons_bound line 146

    Source documentation

    Uniform add/delete control does not depend on the mark dimension or type.

    theorem root_cons_bound (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I) (i : I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) {C : ℝ}
        (hfactor : ∀ x y, |Real.log (factor i x y)| ≤ C) :
        |root T Q m base (Fin.cons i roots) factor - root T Q m base roots factor| ≤ C := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.root

15. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_factor_stability line 167

    Source documentation

    Typewise log-factor errors sum on the actual root list.

    theorem root_factor_stability (T : KernelTower Ω L)
        (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
        (factor factor' : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (C : I → ℝ) (hC : ∀ i x y, |Real.log (factor i x y) - Real.log (factor' i x y)| ≤ C i) :
        |root T Q m base roots factor - root T Q m base roots factor'| ≤ ∑ q, C (roots q) := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.root, OAI.DilutedSpinGlass.q

16. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_mask_bound line 179

    Source documentation

    Deleting tail types is comparison on a common law, not a change of law.

    theorem root_mask_bound (T : KernelTower Ω L)
        (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (keep : I → Prop) [DecidablePred keep] (C : I → ℝ)
        (hC : ∀ i x y, |Real.log (factor i x y)| ≤ C i) :
        |root T Q m base roots factor -
          root T Q m base roots (fun i x y => if keep i then factor i x y else 1)| ≤
            ∑ q, if keep (roots q) then 0 else C (roots q) := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.root, OAI.DilutedSpinGlass.q

17. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.tower_eq_prod line 204

    Source documentation

    The complete independent row can be integrated as a single finite mark. Its dimension depends on the realized labels, never on a deterministic cutoff.

    theorem tower_eq_prod (roots : Fin k → I) (L : ℕ) (T : KernelTower Ω L)
        (Q : (i : I) → Fin L → FiniteLaw (A i)) :
        tower roots L T Q = KernelTower.prod L T
          (markPrior L (fun d => FiniteLaw.pi (fun j => Q (roots j) d))) := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.HeterogeneousMarks.tower, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.markPrior, OAI.DilutedSpinGlass.FiniteLaw.pi

18. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.physical_eq_fst line 217
19. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_one line 228

    Source documentation

    All unused finite priors integrate out, exactly, even if their dimension varies over the full countable type list.

    theorem root_one (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (base : FinitePath Ω L → ℝ) (roots : Fin k → I) :
        root T Q m base roots (fun _ _ _ => 1) = KernelTower.backwardLog L T m base := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.root, OAI.DilutedSpinGlass.KernelTower.backwardLog

20. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_base_bound line 241

    Source documentation

    The pathwise perturbation cost is additive over all realized labels.

    theorem root_base_bound (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (C : I → ℝ) (hC : ∀ i x y, |Real.log (factor i x y)| ≤ C i) :
        |root T Q m base roots factor - KernelTower.backwardLog L T m base| ≤
          ∑ q, C (roots q) := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.root, OAI.DilutedSpinGlass.KernelTower.backwardLog, OAI.DilutedSpinGlass.q

21. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.abs_root_le line 253

    Source documentation

    No lower bound on a type's intensity occurs in this global domination.

    theorem abs_root_le (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) {C : ℝ}
        (hC : ∀ i x y, |Real.log (factor i x y)| ≤ C) :
        |root T Q m base roots factor| ≤ |KernelTower.backwardLog L T m base| + C*k := by
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.root, OAI.DilutedSpinGlass.KernelTower.backwardLog