SizeSpinRoot.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.extension_sampling_dependent line 16
Source documentation
Fresh insertion with a genuinely arbitrary retained-old/test-new joint observable, derived from the actual extension law by finite disintegration.
```
theorem extension_sampling_dependent {n : ℕ} (S : PrescribedTree n)
    (T : KernelTower Ω n) (v : S.Internal)
    (F : Sample Ω S → FinitePath Ω n → ℝ) :
    ((grow S v).sampleLaw T).expect (fun x => F (oldSample S v x) (newPath S v x)) =
      (S.sampleLaw T).expect (fun x => freshEval S T v (F x) x) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath, OAI.DilutedSpinGlass.PrescribedTree.freshEval
lemma OAI.DilutedSpinGlass.PrescribedTree.fresh_square_difference line 39
Source documentation
Squared old/new difference: the same arbitrary old joint law is retained.
```
lemma fresh_square_difference {n : ℕ} (S : PrescribedTree n)
    (T : KernelTower Ω n) (v : S.Internal) (F : Sample Ω S → ℝ)
    (D : Sample Ω S → FinitePath Ω n → ℝ) :
    ((grow S v).sampleLaw T).expect
      (fun x => (F (oldSample S v x) - D (oldSample S v x) (newPath S v x))^2) =
      (S.sampleLaw T).expect (fun x => freshEval S T v (fun y => (F x-D x y)^2) x) :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath, OAI.DilutedSpinGlass.PrescribedTree.freshEval
def OAI.DilutedSpinGlass.SizeCoupling.spinRoot line 61
Source documentation
Literal finite perturbed spin root with one independent mark prior for each realized perturbation. The final spin prior is uniform; earlier spin kernels are dummy point masses. No physical or mark law is replaced.
```
noncomputable def spinRoot {N p k l r : ℕ} {A : Fin l → Type}
    [∀ i, Fintype (A i)]
    (Q : (i : Fin l) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
    (theta : Fin k → InteractionSample p) (h : Fin N → ℝ)
    (indices : Fin k → Fin p → Fin N) (sites : Fin l → Fin N)
    (ψ : (i : Fin l) → Spin → FinitePath (A i) (r+1) → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.SizeCoupling.indicator_sum_ge_one line 71
lemma OAI.DilutedSpinGlass.SizeCoupling.interaction_coupling_bound line 79
lemma OAI.DilutedSpinGlass.SizeCoupling.energy_coupling_bound line 100

theorem OAI.DilutedSpinGlass.SizeCoupling.spinRoot_size_coupling line 129

Source documentation

Keeping exactly the same realized physical and mark samples, only the uniformly coupled sites that hit the new spin can change the root.

theorem spinRoot_size_coupling {N p k l r : ℕ} {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) → ℝ)
    (z : Fin k → Fin p → Fin (N+1) × Fin N) (w : Fin l → Fin (N+1) × Fin N)
    (ψ : (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) :
    |spinRoot Q m theta h (fun j q => newIndex (z j q)) (fun i => newIndex (w i)) ψ -
      spinRoot Q m theta (fun i => h i.succ) (fun j q => oldIndex (z j q))
        (fun i => oldIndex (w i)) ψ| ≤
      |h 0|+2*C*(∑ j, ∑ q, if (z j q).1 = 0 then (1:ℝ) else 0)+
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.spinRoot, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.SizeCoupling.newIndex, OAI.DilutedSpinGlass.SizeCoupling.oldIndex

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.tower_pullback line 175
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.physical_pullback line 188
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.mark_pullback line 196

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_pullback line 205

Source documentation

Mere relabeling preserves every realized heterogeneous prior and factor. This is used to identify per-occurrence and dictionary-label presentations.

theorem root_pullback (f : J → I) {k L : ℕ} (roots : Fin k → J)
    (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
    (base : FinitePath Ω L → ℝ)
    (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) :
    root T (fun j => Q (f j)) m base roots (fun j => factor (f j)) =
      root T Q m base (f ∘ roots) factor := by
…

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

def OAI.DilutedSpinGlass.PrescribedTree.spatialSplitChange line 230
Source documentation
The literal spatial squared norm of the change when this one split moves from d to d+1.
```
noncomputable def spatialSplitChange (k : ℕ+) (C : Fin k → PrescribedTree n)
    (r : ℕ) (T : KernelTower Ω (n+r+1)) (f : FinitePath Ω (n+r+1) → Fin N → ℝ)
    (d : Fin r) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.PrescribedTree.spatialSplitChange_nonneg line 236
theorem OAI.DilutedSpinGlass.PrescribedTree.sum_spatialSplitChange_le line 241
theorem OAI.DilutedSpinGlass.PrescribedTree.averaged_spatialSplitChange_le line 257
def OAI.DilutedSpinGlass.PrescribedTree.stemMeanAt line 281
Source documentation
On the SAME full sampled path, the true conditional mean of a fixed later tree at each depth of its initial unary stretch.
```
noncomputable def stemMeanAt (S : PrescribedTree n) : (r : ℕ) → Fin (r+1) →
    KernelTower Ω (n+r) → (FinitePath Ω (n+r) → ℝ) → FinitePath Ω (n+r) → ℝ
  | 0, _, T, f, _ => treeMean S T f
  | r+1, d, T, f, x => Fin.cases (treeMean (stem S (r+1)) T f)
      (fun e => stemMeanAt S r e (T.2 x.1) (fun y => f (x.1,y)) x.2) d
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.treeMean, OAI.DilutedSpinGlass.PrescribedTree.stem
lemma OAI.DilutedSpinGlass.PrescribedTree.stemMeanAt_zero line 287
lemma OAI.DilutedSpinGlass.PrescribedTree.stemMeanAt_succ line 291
def OAI.DilutedSpinGlass.PrescribedTree.stemIncrementSq line 298
Source documentation
The actual squared L2 martingale increment at depth d.
```
noncomputable def stemIncrementSq (S : PrescribedTree n) (r : ℕ)
    (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → ℝ) (d : Fin r) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.PrescribedTree.stemIncrementSq_nonneg line 303
lemma OAI.DilutedSpinGlass.PrescribedTree.stemIncrementSq_zero line 307
lemma OAI.DilutedSpinGlass.PrescribedTree.stemIncrementSq_succ line 324
theorem OAI.DilutedSpinGlass.PrescribedTree.sum_stemIncrementSq_eq line 335
Source documentation
Exact orthogonality/telescoping identity for the literal conditional means. Increments are compared on the same sampled prefix.
```
theorem sum_stemIncrementSq_eq (S : PrescribedTree n) (r : ℕ)
    (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → ℝ) :
    (∑ d : Fin r, stemIncrementSq S r T f d)=tailVariance S r T f := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.stemIncrementSq, OAI.DilutedSpinGlass.PrescribedTree.tailVariance
theorem OAI.DilutedSpinGlass.PrescribedTree.sum_stemIncrementSq_le_one line 349
Source documentation
Scalar decor:martingale-energy, with no kernel or population-size constant and no assumed filtration theorem.
```
theorem sum_stemIncrementSq_le_one (S : PrescribedTree n) (r : ℕ)
    (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → ℝ) (hf : ∀ x, |f x|≤1) :
    (∑ d : Fin r, stemIncrementSq S r T f d) ≤ 1 := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.stemIncrementSq
theorem OAI.DilutedSpinGlass.PrescribedTree.averaged_stemIncrementSq_le line 357
Source documentation
Any regular subdomain may be used with the exact 1/L ranged-depth normalization. Directions outside it are not renormalized.
```
theorem averaged_stemIncrementSq_le (S : PrescribedTree n) (r L : ℕ)
    (U : Finset (Fin r)) (T : KernelTower Ω (n+r))
    (f : FinitePath Ω (n+r) → ℝ) (hf : ∀ x, |f x|≤1) :
    (∑ d ∈ U, stemIncrementSq S r T f d)/(L:ℝ) ≤ 1/(L:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.stemIncrementSq