FullCubeConditionalContinuity.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.UniversalDictionary.gridExponents line 15
Source documentation
The interior grid exponents; the automatically adjoined root exponent is zero.
```
noncomputable def gridExponents (L : ℕ) : Fin (L+1) → ℝ :=
…
```
lemma OAI.DilutedSpinGlass.UniversalDictionary.gridExponents_cons line 18
lemma OAI.DilutedSpinGlass.UniversalDictionary.gridExponents_lower line 25
lemma OAI.DilutedSpinGlass.UniversalDictionary.gridExponents_mono line 32
lemma OAI.DilutedSpinGlass.UniversalDictionary.gridExponents_last line 37
lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalSingletonEnergy_nonneg line 41
def OAI.DilutedSpinGlass.UniversalDictionary.regularSingletonDepths line 49
Source documentation
The singleton depth domain of the manuscript, with no artificial normalization by its cardinality. At height L+1 its mass is at most one.
```
noncomputable def regularSingletonDepths (L : ℕ) (η : ℝ) : Finset (Fin (L+1)) :=
…
```
theorem OAI.DilutedSpinGlass.UniversalDictionary.singleton_grid_selection line 53

theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_conditional_positive_shift_le line 113

Source documentation

A genuine positive one-step shift is the cyclic coordinate permutation on the regular domain; its wrap-around part is absent, not discarded.

theorem averaged_conditional_positive_shift_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))
    (η : ℝ) (hlarge : 1<η*(L:ℝ)) (D : (α → Fin L) → Prop)
    (hD : ∀ Q, D Q → ∀ j, Admissible (C j) (fun v => (Q (e j v)).val) p L ∧
      DepthAverage.Regular η (fun v => Q (e j v)))
    (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 => (Q (e j v)).val+1) T f)
      (conditionalScheduledProduct M 0 p C (fun j v => (Q (e j v)).val) T f)) ≤
      (Fintype.card ι:ℝ)*∑ j, (Fintype.card (C j).Vertex:ℝ)*
        (∑ v : (C j).Vertex, (vertexArity (C j) v:ℝ)^2)/(L:ℝ) := by
…

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

theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_fullCube_schedule_le line 145

Source documentation

Simultaneous proper-child shift at the ACTUAL next evaluation depth, on the full parent cube. Its spacetime marginal is a single-copy one.

theorem averaged_fullCube_schedule_le (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 : KernelTower Ω L) (f : FinitePath Ω L → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    DepthAverage.average D (fun Q => projectorChangeSq T
      (conditionalScheduledProduct L 0 ((Q a).val+1) C (fun j v => (Q (e j v)).val+1) T f)
      (conditionalScheduledProduct L 0 ((Q a).val+1) C (fun j v => (Q (e j v)).val) T f)) ≤
      (Fintype.card ι:ℝ)*∑ j, (Fintype.card (C j).Vertex:ℝ)*
        (∑ v : (C j).Vertex, (vertexArity (C j) v:ℝ)^2)/(L:ℝ) := by
…

theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_fullCube_evaluation_le line 170
Source documentation
Change the common evaluation depth back by one in the same physical path, while EVERY proper-child branching coordinate is fixed. The terminal case of leaf children uses a full unary stretch of length L.
```
theorem averaged_fullCube_evaluation_le (a : α) (C : ι → ReducedTopology)
    (e : (j : ι) → (C j).Vertex → {j : α // j≠a})
    (D : (α → Fin L) → Prop)
    (hD : ∀ Q, D Q → ∀ j v, (Q a).val<(Q (e j v)).val)
    (T : KernelTower Ω L) (f : FinitePath Ω L → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    DepthAverage.average D (fun Q => projectorChangeSq T
      (conditionalScheduledProduct L 0 ((Q a).val+1) C (fun j v => (Q (e j v)).val) T f)
      (conditionalScheduledProduct L 0 (Q a).val C (fun j v => (Q (e j v)).val) T f)) ≤
      (Fintype.card ι:ℝ)^2/(L:ℝ) := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.ReducedTopology.projectorChangeSq, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct