HistorySelector.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_projection line 16

Source documentation

Exact transport of the finite history expansion through an old-sample projection which commutes with deleting the newly grown branch.

lemma labeledHistory_projection {n : ℕ} {C ι : Type} [DecidableEq C] [DecidableEq ι]
    (m : Fin (n+1) → ℝ)
    (V : (S : PrescribedTree n) → (C → S.Leaf) → (Sample (Ω×Λ) S → ℝ) → ℝ)
    (W : (S : PrescribedTree n) → (C → S.Leaf) → (Sample Ω S → ℝ) → ℝ)
    (hVW : ∀ S pos f, V S pos (fun x => f (sampleFst S x)) = W S pos f)
    (cs : List C) (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
    (pos : C → S.Leaf) (f : Sample Ω S → ℝ) :
    labeledHistory m V cs S U loc pos (fun x => f (sampleFst S x)) =
      labeledHistory m W cs S U loc pos f := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.sampleFst, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory

theorem OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_mark_selector line 43

Source documentation

Mark integration selects the specified sharing constraints, history by history, without changing any signed coefficients or the old reservoir.

theorem labeledHistory_mark_selector {n : ℕ} {C R ι : Type}
    [Fintype C] [DecidableEq C] [Fintype R] [DecidableEq R] [DecidableEq ι]
    (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (a b : R → C) (d : R → Fin n) (spinColor : C → FinitePath Ω n → ℝ)
    (cs : List C) (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
    (pos : C → S.Leaf) (f : Sample Ω S → ℝ) :
    labeledHistory m (fun S pos f =>
      (S.sampleLaw (KernelTower.prod n T
        (markPrior n (fun _ => FiniteLaw.pi (fun _ : R => MarkSelector.rademacher))))).expect
      (fun x => f x * ∏ c, spinColor c (KernelTower.pathFst n (S.pathAt (pos c) x)) *
        MarkSelector.pathColor a b d c (KernelTower.pathSnd n (S.pathAt (pos c) x))))
      cs S U loc pos (fun x => f (sampleFst S x)) =
…

theorem OAI.DilutedSpinGlass.PrescribedTree.coloredAt_mark_selector line 66
lemma OAI.DilutedSpinGlass.PrescribedTree.historyMass_mul line 99
theorem OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_abs_le_mass line 118
Source documentation
Every literal labeled extension contributes its actual absolute coefficient. The domination retains all old tests rather than replacing the sampled law by an unsigned or independently resampled one.
```
theorem labeledHistory_abs_le_mass (F : PrescribedTree L → ℝ)
    (V : (S : PrescribedTree L) → (C → S.Leaf) → (Sample Ω S → ℝ) → ℝ)
    (hV : ∀ S pos f, (∀ x, |f x| ≤ 1) → |V S pos f| ≤ F S)
    (cs : List C) (S : PrescribedTree L) (U : Finset ι) (loc : ι → S.Leaf)
    (pos : C → S.Leaf) (f : Sample Ω S → ℝ) (hf : ∀ x, |f x| ≤ 1) :
    |labeledHistory (grid L 0 L) V cs S U loc pos f| ≤ historyMass F cs.length S U.card := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.historyMass

theorem OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_charging_bound line 155

Source documentation

Charging estimate for an actual labeled terminal observable. Restricting the allowed splitting matrices and inserting a uniformly bounded projection error are both handled in this single estimate.

theorem labeledHistory_charging_bound (hL : 0 < L) (Q : Finset ℕ) (b : ℕ)
    (V : (S : PrescribedTree L) → (C → S.Leaf) → (Sample Ω S → ℝ) → ℝ)
    (E : ℝ) (hE : 0 ≤ E) (cs : List C) (S : PrescribedTree L)
    (U : Finset ι) (loc : ι → S.Leaf) (pos : C → S.Leaf)
    (f : Sample Ω S → ℝ) (hf : ∀ x, |f x| ≤ 1) (hU : U.card ≤ leaves S)
    (hV : ∀ T pos g, (∀ x, |g x| ≤ 1) → |V T pos g| ≤ E *
      (if branchingCount S (· ∈ Q)+b ≤ branchingCount T (· ∈ Q) then 1 else 0)) :
    |labeledHistory (grid L 0 L) V cs S U loc pos f| ≤
      E * (chargeBound (2*(leaves S+cs.length:ℕ)) ((Q.card:ℝ)*(leaves S+cs.length:ℕ))
        cs.length b * (L:ℝ)⁻¹^b) := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.chargeBound

theorem OAI.DilutedSpinGlass.PrescribedTree.matrix_paths_expect line 184

Source documentation

Complete positional splitting matrices determine the full joint path law, not just pair overlaps. The enumerating colors may repeat leaf positions.

theorem matrix_paths_expect (T S : PrescribedTree n) (q : C → T.Leaf)
    (hq : Function.Surjective q) (pos : C → S.Leaf)
    (h : ∀ a b, splitDepth S (pos a) (pos b) = splitDepth T (q a) (q b))
    (K : KernelTower Ω n) (F : (C → FinitePath Ω n) → ℝ) :
    (S.sampleLaw K).expect (fun x => F (fun c => S.pathAt (pos c) x)) =
      (T.sampleLaw K).expect (fun x => F (fun c => T.pathAt (q c) x)) := by
…

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

theorem OAI.DilutedSpinGlass.PrescribedTree.matrix_weighted_error line 205

Source documentation

An arbitrary correlated old test bounded by one costs at most the actual single-target L2 error, since the entire target marginal is fixed.

theorem matrix_weighted_error (T S : PrescribedTree n) (q : C → T.Leaf)
    (hq : Function.Surjective q) (pos : C → S.Leaf)
    (h : ∀ a b, splitDepth S (pos a) (pos b) = splitDepth T (q a) (q b))
    (K : KernelTower Ω n) (D : (C → FinitePath Ω n) → ℝ)
    (f : Sample Ω S → ℝ) (hf : ∀ x, |f x| ≤ 1) :
    |(S.sampleLaw K).expect (fun x => f x * D (fun c => S.pathAt (pos c) x))| ≤
      (T.sampleLaw K).l2 (fun x => D (fun c => T.pathAt (q c) x)) := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample