TensorWardError.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Finite covariance derivative contractions in the tensor perturbation error of the spectral Ward identity (manuscript, §3, lines 421--439).

def OAI.InvariantIsing.projectedOverlapEndpointDerivative line 17
lemma OAI.InvariantIsing.hasDerivAt_mixedProjectedOverlap_plane line 22
def OAI.InvariantIsing.spectralMonomialEndpointCoefficient line 34
def OAI.InvariantIsing.spectralMonomialEndpointDerivative line 39
theorem OAI.InvariantIsing.hasDerivAt_spectralMonomial_mixed_plane line 45
Source documentation
This is the derivative in one tensor endpoint. The other endpoint and all tree coordinates remain fixed during the plane rotation.
```
theorem hasDerivAt_spectralMonomial_mixed_plane {N m : ℕ} (U : Orthogonal N)
    (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ) (i j : Fin N) (σ τ : Spin N) :
    HasDerivAt (fun s => ∏ a,
      mixedProjectedOverlap (matrixRotation (planeRotation i j s * U)) (matrixRotation U) (I a) σ τ ^ d a)
      (spectralMonomialEndpointDerivative U I d i j σ τ) 0 := by
…
```
Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.mixedProjectedOverlap, OAI.InvariantIsing.matrixRotation, OAI.InvariantIsing.planeRotation, OAI.InvariantIsing.spectralMonomialEndpointDerivative
theorem OAI.InvariantIsing.hasDerivAt_spectralTensor_cross_plane line 59
lemma OAI.InvariantIsing.jointSpectralMonomialCoefficients_mixed_cross line 74
theorem OAI.InvariantIsing.hasDerivAt_jointSpectralCoefficients_cross_plane line 86
lemma OAI.InvariantIsing.spectralMonomialEndpointCoefficient_abs_le line 102
def OAI.InvariantIsing.projectedEndpointContraction line 119

theorem OAI.InvariantIsing.projectedEndpointContraction_eq line 126

Source documentation

The two coordinate sums contract into products of normalized projected inner products, with one remaining factor 1/N.

theorem projectedEndpointContraction_eq {N : ℕ} (U : Orthogonal N)
    (I J K : Finset (Fin N)) (η θ σ τ : Spin N) :
    projectedEndpointContraction U I J K η θ σ τ =
      (N : ℝ)⁻¹ * (projectedOverlap (matrixRotation U) (I ∩ K) η τ *
        projectedOverlap (matrixRotation U) J θ σ -
        projectedOverlap (matrixRotation U) I η σ * projectedOverlap (matrixRotation U) (J ∩ K) θ τ) := by
…

Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.projectedEndpointContraction, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.matrixRotation

theorem OAI.InvariantIsing.projectedEndpointContraction_abs_le line 153
def OAI.InvariantIsing.spectralMonomialEndpointContraction line 169
theorem OAI.InvariantIsing.spectralMonomialEndpointContraction_eq line 175
theorem OAI.InvariantIsing.spectralMonomialEndpointContraction_abs_le line 193
def OAI.InvariantIsing.tensorWardPerturbationError line 210
theorem OAI.InvariantIsing.tensorWardPerturbationError_eq line 217
theorem OAI.InvariantIsing.hasDerivAt_tensorPerturbation_cross_plane line 238
theorem OAI.InvariantIsing.hasDerivAt_jointTensorPerturbation_cross_plane line 252

theorem OAI.InvariantIsing.tensorWardPerturbationError_abs_le line 272

Source documentation

One covariance contraction after Gaussian integration by parts, for the actual finite geometric-weight perturbation. It is uniform in tree depth, all four spin replicas, and the coordinate groups.

theorem tensorWardPerturbationError_abs_le {N m : ℕ} (hN : 0 < N) (U : Orthogonal N)
    (groups : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ)
    (treeDegree : Fin N → ℕ) (n : ℕ) (u : Fin N → ℝ) (hu : ∀ r, |u r| ≤ 2)
    (D : ℝ) (hD : 0 ≤ D) (hdegree : ∀ r, (∑ a, (degree r a : ℝ)) ≤ D * ((r : ℝ) + 1))
    (I J : Finset (Fin N)) (η θ : Spin N) (x y : Spin N × LabeledLeaf n) :
    |tensorWardPerturbationError U groups degree treeDegree n u I J η θ x y| ≤
      8 * D * perturbationScale N ^ 2 := by
…

Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorWardPerturbationError

theorem OAI.InvariantIsing.tensorWardPerturbationError_test_abs_le line 309