RootProjectionShiftError.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.ReducedTopology.delayed_target_projector line 16
Source documentation
The actual delayed target's own projection is the shifted scheduled proper-child product. No identification of independent pairs of assignments.
```
lemma delayed_target_projector (H r d : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ))
    (C : Fin k → ReducedTopology) (q : (j : Fin k) → (C j).Vertex → ℕ)
    (hq : ∀ j v, r+d+1≤q j v)
    (T : KernelTower Ω (H+1+r+1+d))
    (f : FinitePath Ω (H+1+r+1+d) → Fin N → ℝ) :
    (fun x i => PrescribedTree.splitProjector
      (.node k (fun j => realize H (r+1+d+1) (C j) (fun v => q j v+1)))
      r d T (fun y => f y i) x)=
    conditionalScheduledProduct (H+1+r+1+d) 0 (r+1+d) C (fun j v => q j v+1) T f := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct
theorem OAI.DilutedSpinGlass.ReducedTopology.delayed_target_projection_le line 33
Source documentation
Bound the literal target error in the signed matrix identity by proper children and the ONE extension-uniform h_N on the SAME full depth cube. Target leaf labels may be any bijective spatial-multioverlap enumeration.
```
theorem delayed_target_projection_le (H r d : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ))
    (a : α) (C : Fin k → ReducedTopology)
    (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+r+1+d)) (ha : (Q a).val=r+d)
    (hQ : ∀ j v, (Q a).val+1≤(Q (e j v)).val)
    (T : KernelTower Ω (H+1+r+1+d))
    (f : FinitePath Ω (H+1+r+1+d) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    let Child := fun j => realize H (r+1+d+1) (C j) (fun v => (Q (e j v)).val+1)
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.realize
lemma OAI.DilutedSpinGlass.DepthAverage.average_le_sqrt_average_sq line 82
lemma OAI.DilutedSpinGlass.DepthAverage.integrable_average line 94
lemma OAI.DilutedSpinGlass.DepthAverage.integral_average line 105
theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_projectionShiftError_le line 126

theorem OAI.DilutedSpinGlass.ReducedTopology.root_averaged_projectionShiftError_le line 142

Source documentation

The SAME normalized-cube estimate survives genuine physical-root averaging with no uniformity loss. The root law may have a variable finite alphabet. Only ordinary Bochner integrability is required.

theorem root_averaged_projectionShiftError_le {Z : Type} [MeasurableSpace Z] (μ : Measure Z)
    [IsProbabilityMeasure μ] (Ω : Z → Type) [∀ z, Fintype (Ω z)]
    (a : α) (C : ι → ReducedTopology)
    (e : (j : ι) → (C j).Vertex → {j : α // j≠a}) (he : ∀ j, Function.Injective (e j))
    (η : ℝ) (hlarge : 1<η*(L:ℝ)) (D : (α → Fin L) → Prop)
    (hD : ∀ Q, D Q → ∀ j, Admissible (C j) (fun v => (Q (e j v)).val) ((Q a).val+1) L ∧
      DepthAverage.Regular η (fun v => Q (e j v)))
    (T : (z : Z) → KernelTower (Ω z) L)
    (f : (z : Z) → FinitePath (Ω z) L → Fin N → ℝ) (hf : ∀ z x i, |f z x i|≤1)
    (hI : ∀ Q, Integrable (fun z => projectionShiftError a C e (T z) (f z) Q) μ) :
    DepthAverage.average D (fun Q => ∫ z, projectionShiftError a C e (T z) (f z) Q ∂μ) ≤
      Real.sqrt (8*((Fintype.card ι:ℝ)*(∑ j, (Fintype.card (C j).Vertex:ℝ)*
…

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError, OAI.DilutedSpinGlass.DepthAverage.average