ProperChildScheduleContinuity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.FiniteLaw.spatialSq_product_difference_le line 14

Source documentation

Bounded products are Lipschitz in the actual normalized spatial norm, including the empty spatial dimension convention.

lemma spatialSq_product_difference_le (X Y : ι → Fin N → ℝ)
    (hX : ∀ j i, |X j i|≤1) (hY : ∀ j i, |Y j i|≤1) :
    spatialSq (fun i => (∏ j, X j i)-(∏ j, Y j i)) ≤
      (Fintype.card ι:ℝ)*∑ j, spatialSq (fun i => X j i-Y j i) := by
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw.spatialSq

lemma OAI.DilutedSpinGlass.PrescribedTree.tailMean_node_product line 35
Source documentation
Exact proper-child factorization of the conditional first-split mean; the unary child transition is retained, not erased.
```
lemma tailMean_node_product (k : ℕ+) (C : Fin k → PrescribedTree n) (p : ℕ)
    (T : KernelTower Ω (n+1+p)) (f : FinitePath Ω (n+1+p) → ℝ)
    (x : FinitePath Ω (n+1+p)) :
    tailMean (.node k C) p T f x=∏ j, tailMean (unary (C j)) p T f x := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.tailMean, OAI.DilutedSpinGlass.PrescribedTree.unary
lemma OAI.DilutedSpinGlass.PrescribedTree.splitProjector_node_product line 45
Source documentation
The projector used in the signed multileaf matrix identity is literally the product of proper-child conditional means on the SAME sampled prefix.
```
lemma splitProjector_node_product (k : ℕ+) (C : Fin k → PrescribedTree n) (r d : ℕ)
    (T : KernelTower Ω (n+1+r+1+d)) (f : FinitePath Ω (n+1+r+1+d) → ℝ)
    (x : FinitePath Ω (n+1+r+1+d)) :
    splitProjector (.node k C) r d T f x=∏ j, splitProjector (unary (C j)) r d T f x := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.PrescribedTree.unary
lemma OAI.DilutedSpinGlass.ReducedTopology.tailScheduleChange_nonneg line 62
def OAI.DilutedSpinGlass.ReducedTopology.childScheduleProjection line 70
Source documentation
Product of the actual proper-child schedule projectors, restricted from the parent depth-assignment cube. Coordinates may be independently translated. No independent sampling of aligned copies occurs in this definition.
```
noncomputable def childScheduleProjection (H d p : ℕ) (C : ι → ReducedTopology)
    (e : (j : ι) → (C j).Vertex → α) (τ : (j : ι) → (C j).Vertex → Equiv.Perm (Fin L))
    (s : (j : ι) → (C j).Vertex → Bool)
    (T : KernelTower Ω (H+p)) (f : FinitePath Ω (H+p) → Fin N → ℝ)
    (q : α → Fin L) (x : FinitePath Ω (H+p)) (i : Fin N) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q
lemma OAI.DilutedSpinGlass.ReducedTopology.childScheduleProjection_bound line 79
theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_childScheduleProjection_change_le line 91

theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_childSchedule_target_change_le line 139

Source documentation

Both target vectors may come from any joint history marginal on the parent assignment cube. The bound is the same single-copy proper-child cost.

theorem averaged_childSchedule_target_change_le (H d p : ℕ) (hheight : d+H=L)
    (C : ι → ReducedTopology)
    (e : (j : ι) → (C j).Vertex → α) (he : ∀ j, Function.Injective (e j))
    (τ : (j : ι) → (C j).Vertex → Equiv.Perm (Fin L))
    (η : ℝ) (hlarge : 1<η*(L:ℝ)) (s : (j : ι) → (C j).Vertex → Bool)
    (D : (α → Fin L) → Prop)
    (hD : ∀ q, D q → ∀ j, Admissible (C j) (fun v => (τ j v (q (e j v))).val) d L ∧
      DepthAverage.Regular η (DepthAverage.coordinateProjection (e j) (τ j) q))
    (T : KernelTower Ω (H+p)) (f : FinitePath Ω (H+p) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1)
    (Target : (α → Fin L) → PrescribedTree (H+p))
    (a b : (q : α → Fin L) → (Target q).Leaf) :
    DepthAverage.average D (fun q => PrescribedTree.targetContractionChangeSq (Target q) T (a q) (b q)
…