OAI/Probability/DilutedSpin/MarkInsertion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.rowPerm line 15

   Source documentation

   A relabeling of heterogeneous marks, without identification of their alphabets.

   def rowPerm {k : ℕ} (roots : Fin k → I) (σ : Equiv.Perm (Fin k)) :
       (Ω × Row (A := A) roots) ≃ (Ω × Row (A := A) (roots ∘ σ)) :=
   …

   Mentions: OAI.DilutedSpinGlass.HeterogeneousMarks.Row

2. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.tower_transport line 19
3. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.physical_rowPerm line 39
4. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.mark_rowPerm line 51
5. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.logWeight_rowPerm line 63
6. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_perm line 73
7. def OAI.DilutedSpinGlass.HeterogeneousMarks.treeScore line 85

   Source documentation

   The exact tree-score summand for one term of the full reservoir.

   noncomputable def treeScore (S : PrescribedTree L) (a : S.Leaf)
       (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
       (base : FinitePath Ω L → ℝ) (roots : Fin k → I)
       (factor numerator : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
       (f : (S.Leaf → FinitePath Ω L) → ℝ) (q : Fin k) : ℝ :=
   …

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

8. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.treeScore_perm line 96
9. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.abs_treeScore_le line 117
10. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_update_bound line 150

    Source documentation

    Replacement may change the complete mark alphabet and prior of that term; it is proved by two independent insertions, not by identifying the alphabets.

    theorem root_update_bound (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base : FinitePath Ω L → ℝ) {k : ℕ} (roots : Fin k → I) (q : Fin k) (i : I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) {C : ℝ}
        (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) :
        |root T Q m base (Function.update roots q i) factor - root T Q m base roots factor| ≤ 2*C := by
    …

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

11. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_base_stability line 190

    Source documentation

    Physical disorder changes only the base energy, even with all countably many type laws available to the finite realized auxiliary row.

    theorem root_base_stability (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base base' : FinitePath Ω L → ℝ) {k : ℕ} (roots : Fin k → I)
        (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) {C : ℝ}
        (hb : ∀ x, |base x-base' x| ≤ C) :
        |root T Q m base 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

12. def OAI.DilutedSpinGlass.HeterogeneousMarks.insertedTreeScore line 209

    Source documentation

    Add-one score on an old n-factor model with an independent mark process. The old Gibbs tower includes every one of its original selected-type terms.

    noncomputable def insertedTreeScore (S : PrescribedTree L) (a : S.Leaf)
        (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I) (i : I)
        (factor numerator : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (f : (S.Leaf → FinitePath Ω L) → ℝ) : ℝ :=
    …

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

13. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.treeScore_insertion line 227

    Source documentation

    Literal change-of-variables and successive-tilt proof of the Palm insertion. No conditional factorization of the tilted mark rows is being assumed.

    theorem treeScore_insertion (S : PrescribedTree L) (a : S.Leaf)
        (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I) (i : I)
        (factor numerator : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (f : (S.Leaf → FinitePath Ω L) → ℝ) :
        treeScore S a T Q m base (Fin.cons i roots) factor numerator f 0 =
          insertedTreeScore S a T Q m base roots i factor numerator f := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.treeScore, OAI.DilutedSpinGlass.HeterogeneousMarks.insertedTreeScore

14. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.insertedTreeScore_density line 263

    Source documentation

    Density version of the same identity. The numerator is at the selected anchor and its own new factor occurs exactly once in the denominator.

    theorem insertedTreeScore_density (S : PrescribedTree L) (a : S.Leaf)
        (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin (L+1) → ℝ)
        (hm : ∀ j : Fin L, m j.succ ≠ 0) (hroot : m 0 = 0)
        (base : FinitePath Ω L → ℝ) (roots : Fin k → I) (i : I)
        (factor numerator : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (f : (S.Leaf → FinitePath Ω L) → ℝ) :
        let U := KernelTower.prod L
    …

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

15. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.full_reservoir_palm line 296

    Source documentation

    Full countable-type Palm for the literal tilted tree statistic. Its right side uses the same original reservoir, plus one independently sampled mark.

    theorem full_reservoir_palm {L : ℕ} (S : PrescribedTree L) (a : S.Leaf)
        (s : ℝ≥0) (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
        (m : Fin L → ℝ) (base : FinitePath Ω L → ℝ)
        (factor numerator : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
        (f : (S.Leaf → FinitePath Ω L) → ℝ) {B : ℝ}
        (hf : ∀ x, |f x| ≤ B) (hn : ∀ i y z, |numerator i y z| ≤ 1)
        (hA : ∀ i y z, 1/2 ≤ factor i y z) :
        (∫ n : ℕ, ∫ roots, ∑ q, treeScore S a T Q m base roots factor numerator f q
          ∂Measure.pi (fun _ : Fin n => ν) ∂poissonMeasure s) =
          (s : ℝ) * ∫ n : ℕ, ∫ i, ∫ roots,
            insertedTreeScore S a T Q m base roots i factor numerator f
              ∂Measure.pi (fun _ : Fin n => ν) ∂ν ∂poissonMeasure s := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.HeterogeneousMarks.treeScore, OAI.DilutedSpinGlass.HeterogeneousMarks.insertedTreeScore