OAI/Probability/DilutedSpin/ActualPrefix.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.FinitePath.Agree line 11

   Source documentation

   Equality of the first e sampled coordinates (root variables are held fixed).

   def Agree {Ω : Type} : (e : ℕ) → {n : ℕ} → FinitePath Ω n → FinitePath Ω n → Prop
     | 0, _, _, _ => True
     | _+1, 0, _, _ => True
     | e+1, _+1, x, y => x.1 = y.1 ∧ Agree e x.2 y.2

   Mentions: OAI.DilutedSpinGlass.FinitePath

2. theorem OAI.DilutedSpinGlass.FinitePath.Agree.refl line 16
3. def OAI.DilutedSpinGlass.FinitePath.PrefixFunction line 25
4. theorem OAI.DilutedSpinGlass.PrescribedTree.paths_agree line 38

   Source documentation

   Shared labeled prefixes have identical samples even when leaf values collide elsewhere. This is only an implication from POSITION to sampled values.

   theorem paths_agree {n : ℕ} (S : PrescribedTree n) (a b : Leaf S)
       (x : Sample Ω S) (e : ℕ) (he : e ≤ splitDepth S a b) :
       FinitePath.Agree e (pathAt S a x) (pathAt S b x) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.FinitePath.Agree, OAI.DilutedSpinGlass.PrescribedTree.pathAt

5. theorem OAI.DilutedSpinGlass.PrescribedTree.fresh_path_agrees line 61

   Source documentation

   The fresh path shares precisely the retained old prefix stipulated by its uncontracted divergence vertex.

   theorem fresh_path_agrees {n : ℕ} (S : PrescribedTree n) (v : Internal S)
       (a : Leaf S) (x : Sample Ω (grow S v)) (e : ℕ)
       (he : e ≤ freshSplitDepth S v a) :
       FinitePath.Agree e (newPath S v x) (pathAt S a (oldSample S v x)) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.FinitePath.Agree, OAI.DilutedSpinGlass.PrescribedTree.newPath, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.oldSample

6. theorem OAI.DilutedSpinGlass.PrescribedTree.prefix_choices_total line 71

   Source documentation

   All old-or-fresh choices following an old prefix through depth e have total coefficient m_e. This includes all descendants, not only fresh unary branches.

   theorem prefix_choices_total {n : ℕ} (S : PrescribedTree n) (a : Leaf S)
       (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1)
       (e : ℕ) (he : e ≤ n) :
       (∑ b : Leaf S, if e ≤ splitDepth S b a then (1:ℝ) else 0) +
         (∑ v : Internal S, if e ≤ freshSplitDepth S v a then gamma S m v else 0) =
           m ⟨e,by omega⟩ := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.PrescribedTree.gamma

7. theorem OAI.DilutedSpinGlass.PrescribedTree.prefix_choices_expectation line 120

   Source documentation

   Exact joint marginal for the prefix-through-e class. Multiplication by an arbitrary old test is retained throughout, as required in decorrelation: the new path may be a reused old leaf or any fresh descendant of the prefix.

   theorem prefix_choices_expectation {n : ℕ} (S : PrescribedTree n) (K : KernelTower Ω n)
       (a : Leaf S) (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1)
       (e : ℕ) (he : e ≤ n) (D : FinitePath Ω n → ℝ) (hD : FinitePath.PrefixFunction e D)
       (H : Sample Ω S → ℝ) :
       (∑ b : Leaf S, if e ≤ splitDepth S b a then
         (sampleLaw S K).expect (fun x => H x * D (pathAt S b x)) else 0) +
       (∑ v : Internal S, if e ≤ freshSplitDepth S v a then
         gamma S m v * (sampleLaw (grow S v) K).expect
           (fun x => H (oldSample S v x) * D (newPath S v x)) else 0) =
       m ⟨e,by omega⟩ * (sampleLaw S K).expect (fun x => H x * D (pathAt S a x)) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.FinitePath.PrefixFunction, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath

8. theorem OAI.DilutedSpinGlass.FiniteLaw.abs_expect_le_expect_abs line 168
9. def OAI.DilutedSpinGlass.SizeCoupling.spinMean line 181
10. theorem OAI.DilutedSpinGlass.SizeCoupling.expected_total_new_count line 191
11. theorem OAI.DilutedSpinGlass.SizeCoupling.spinMean_size_coupling line 206

    Source documentation

    Exact with-replacement uniform-site coupling estimate before averaging physical disorder or mark specifications. Both finite-size marginals are the actual independent index laws.

    theorem spinMean_size_coupling {N p k l r : ℕ} [NeZero N] {A : Fin l → Type}
        [∀ i, Fintype (A i)]
        (Q : (i : Fin l) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
        (hm : ∀ j, 0 < m j) (theta : Fin k → InteractionSample p) (h : Fin (N+1) → ℝ)
        (ψ : (i : Fin l) → Spin → FinitePath (A i) (r+1) → ℝ)
        {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D)
        (hθ : ∀ j σ, |(theta j).1 σ| ≤ C) (hψ : ∀ i σ a, |Real.log (ψ i σ a)| ≤ D) :
        |spinMean Q m theta h ψ-spinMean Q m theta (fun i => h i.succ) ψ| ≤
          |h 0|+2*C*k*p/(N+1)+2*D*l/(N+1) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.spinMean

12. lemma OAI.DilutedSpinGlass.bounded_product_one_difference_sq line 271
13. theorem OAI.DilutedSpinGlass.PrescribedTree.treeMean_node_one_difference_sq line 287
14. inductive OAI.DilutedSpinGlass.PrescribedTree.TreeContext line 305

    Source documentation

    A literal prescribed-tree context with one designated descendant hole; sibling branches are retained as genuine shapes, not erased from the test.

    inductive TreeContext (h : ℕ) : ℕ → Type
      | hole : TreeContext h h
      | node {n : ℕ} (k : ℕ+) (C : Fin k → PrescribedTree n) (i : Fin k)
          (inner : TreeContext h n) : TreeContext h (n+1)

    Mentions: OAI.DilutedSpinGlass.PrescribedTree

15. def OAI.DilutedSpinGlass.PrescribedTree.TreeContext.plug line 310
16. theorem OAI.DilutedSpinGlass.PrescribedTree.TreeContext.sum_difference_le line 317

    Source documentation

    Propagation to ANY ancestor contracts the total squared difference. Precisely one sampled prefix remains after the other branches integrate out. The uniform family estimate is applied to the actual tower at that prefix.

    theorem TreeContext.sum_difference_le {h n : ℕ} {ι : Type*} [Fintype ι]
        (ctx : TreeContext h n) (S D : ι → PrescribedTree h) (B : ℝ)
        (hB : ∀ (T : KernelTower Ω h) (f : FinitePath Ω h → ℝ), (∀ x, |f x| ≤ 1) →
          (∑ i, (treeMean (S i) T f-treeMean (D i) T f)^2) ≤ B) :
        ∀ (T : KernelTower Ω n) (f : FinitePath Ω n → ℝ), (∀ x, |f x| ≤ 1) →
          (∑ i, (treeMean (ctx.plug (S i)) T f-treeMean (ctx.plug (D i)) T f)^2) ≤ B := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree.TreeContext, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean

17. theorem OAI.DilutedSpinGlass.PrescribedTree.contextual_split_shift_le line 346