CoordinateFiber.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.DepthAverage.depthLaw_split line 13
theorem OAI.DilutedSpinGlass.DepthAverage.coordinate_fiber_bound line 29
lemma OAI.DilutedSpinGlass.updateCoordinate_update line 48
lemma OAI.DilutedSpinGlass.DepthAverage.splitAt_values_update line 61
def OAI.DilutedSpinGlass.ReducedTopology.vertexChangeSq line 80
Source documentation
Actual change in the conditional tree mean when one assigned vertex moves by one grid step. All remaining topology coordinates are unchanged.
```
noncomputable def vertexChangeSq (H d : ℕ) (S : ReducedTopology) (v : S.Vertex)
    (T : KernelTower Ω H) (f : FinitePath Ω H → ℝ) (q : S.Vertex → Fin L) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q
lemma OAI.DilutedSpinGlass.ReducedTopology.vertexChangeSq_nonneg line 87
theorem OAI.DilutedSpinGlass.ReducedTopology.averaged_vertexChangeSq_le line 92
def OAI.DilutedSpinGlass.FiniteLaw.spatialSq line 146
Source documentation
Squared normalized spatial norm, with the original zero-size convention.
```
noncomputable def spatialSq (x : Fin N → ℝ) : ℝ := (∑ i, (x i)^2)/(N:ℝ)
```
lemma OAI.DilutedSpinGlass.FiniteLaw.spatialSq_nonneg line 148
lemma OAI.DilutedSpinGlass.FiniteLaw.spatial_mean_sq_le line 151
theorem OAI.DilutedSpinGlass.FiniteLaw.dot_pair_change_sq line 168
Source documentation
The simultaneous change of both vectors in a contraction is controlled by the two actual coupled spatial norms, regardless of correlation.
```
theorem dot_pair_change_sq (x y u v : Fin N → ℝ)
    (hx : ∀ i, |x i|≤1) (hy : ∀ i, |y i|≤1)
    (hu : ∀ i, |u i|≤1) (hv : ∀ i, |v i|≤1) :
    (dot x y-dot u v)^2 ≤ 2*spatialSq (fun i => x i-u i)+2*spatialSq (fun i => y i-v i) := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.FiniteLaw.spatialSq
theorem OAI.DilutedSpinGlass.PrescribedTree.coupled_projection_change_l2 line 199
Source documentation
A target contraction change costs only the single-path marginal spatial change. This is uniform over the entire target shape and does NOT assume regularity of a union with any old tree.
```
theorem coupled_projection_change_l2 (S : PrescribedTree n) (T : KernelTower Ω n)
    (a b : S.Leaf) (X Y : FinitePath Ω n → Fin N → ℝ)
    (hX : ∀ x i, |X x i|≤1) (hY : ∀ x i, |Y x i|≤1) :
    (S.sampleLaw T).l2 (fun z => FiniteLaw.dot (X (S.pathAt a z)) (X (S.pathAt b z))-
      FiniteLaw.dot (Y (S.pathAt a z)) (Y (S.pathAt b z))) ≤
      2*Real.sqrt ((KernelTower.law n T).expect (fun x => FiniteLaw.spatialSq (fun i => X x i-Y x i))) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.FiniteLaw.spatialSq
theorem OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_change_spatial line 224
Source documentation
The full target matrix error splits into its genuine proper-child projection and a shape-independent single-path coupled comparison.
```
theorem matrixProjectionError_change_spatial (S : PrescribedTree n) (q : I → S.Leaf)
    (T : KernelTower Ω n) (a c : I) (A : (I → FinitePath Ω n) → ℝ)
    (X Y : FinitePath Ω n → Fin N → ℝ)
    (hX : ∀ x i, |X x i|≤1) (hY : ∀ x i, |Y x i|≤1) :
    matrixProjectionError S q T a c A X ≤ matrixProjectionError S q T a c A Y +
      2*Real.sqrt ((KernelTower.law n T).expect (fun x => FiniteLaw.spatialSq (fun i => Y x i-X x i))) :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.FiniteLaw.spatialSq