ConditionalSpatialContinuity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.ReducedTopology.projectorChangeSq line 14
Source documentation
Single-copy spatial squared distance of two actual conditional means.
```
noncomputable def projectorChangeSq {M : ℕ} (T : KernelTower Ω M)
    (X Y : FinitePath Ω M → Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.ReducedTopology.projectorChangeSq_nonneg line 18
lemma OAI.DilutedSpinGlass.ReducedTopology.projectorChangeSq_symm line 22
lemma OAI.DilutedSpinGlass.ReducedTopology.projectorChangeSq_triangle line 27

theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_conditional_schedule_change_le line 47

Source documentation

Fixed-prefix simultaneous child-shift continuity, stated on the actual full-horizon conditional products. The horizon equality is a reindexing only.

theorem averaged_conditional_schedule_change_le (M H p : ℕ) (htotal : M=H+p)
    (hheight : p+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) p L ∧
      DepthAverage.Regular η (DepthAverage.coordinateProjection (e j) (τ j) Q))
    (T : KernelTower Ω M) (f : FinitePath Ω M → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    DepthAverage.average D (fun Q => projectorChangeSq T
      (conditionalScheduledProduct M 0 p C (fun j v => (τ j v (Q (e j v))).val) T f)
      (conditionalScheduledProduct M 0 p C
…

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.DepthAverage.coordinateProjection, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.ReducedTopology.projectorChangeSq, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct

theorem OAI.DilutedSpinGlass.ReducedTopology.conditional_evaluation_sum_le line 74
Source documentation
Full-horizon evaluation martingale energy before the first child split, in the actual single-copy spatial norm, with arbitrary retained subdomain.
```
theorem conditional_evaluation_sum_le (M n r : ℕ) (htotal : M=n+r)
    (C : ι → ReducedTopology) (q : (j : ι) → (C j).Vertex → ℕ)
    (hq : ∀ j v, r≤q j v) (U : Finset (Fin r))
    (T : KernelTower Ω M) (f : FinitePath Ω M → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    (∑ t ∈ U, projectorChangeSq T
      (conditionalScheduledProduct M 0 (t.val+1) C q T f)
      (conditionalScheduledProduct M 0 t.val C q T f))/(L:ℝ) ≤ (Fintype.card ι:ℝ)^2/(L:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.projectorChangeSq, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct