OAI/Probability/InvariantIsing/Arrays/TensorCoefficientDerivative.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Coordinate-plane derivatives of the actual finite spectral tensor coefficients, with uniform finite-dimensional bounds for Haar differentiation.

  1. def OAI.InvariantIsing.spectralSpinPlaneDerivative line 17

    Source documentation

    A normalized spectral coordinate has a uniformly bounded plane derivative.

    def spectralSpinPlaneDerivative {N : ℕ} (U : Orthogonal N) (σ : Spin N)
    (i j a : Fin N) : ℝ :=
…

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

  2. lemma OAI.InvariantIsing.abs_normalized_spinCoordinate_le_one line 22
  3. lemma OAI.InvariantIsing.spectralSpinFeature_abs_le_one line 34
  4. lemma OAI.InvariantIsing.spectralSpinPlaneDerivative_abs_le line 39
  5. lemma OAI.InvariantIsing.hasDerivAt_spectralSpinFeature_plane line 52
  6. def OAI.InvariantIsing.spectralTensorPlaneDerivative line 63

    Source documentation

    The ordinary product-rule derivative of one spectral tensor feature.

    def spectralTensorPlaneDerivative {N m : ℕ} (U : Orthogonal N)
    (I : Fin m → Finset (Fin N)) (d : Fin m → ℕ) (σ : Spin N)
    (i j : Fin N) (v : SpectralTensorIndex I d) : ℝ :=
…

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

  7. lemma OAI.InvariantIsing.hasDerivAt_spectralMonomialFeature_plane line 72
  8. lemma OAI.InvariantIsing.spectralTensorPlaneDerivative_abs_le line 83
  9. lemma OAI.InvariantIsing.measurable_spectralSpinPlaneDerivative line 123
  10. lemma OAI.InvariantIsing.measurable_spectralTensorPlaneDerivative line 132
  11. def OAI.InvariantIsing.spinTensorPlaneDerivative line 147

    Source documentation

    The independent linear enrichment has zero rotation derivative.

    def spinTensorPlaneDerivative {N m k : ℕ} (U : Orthogonal N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (σ : Spin N) (i j : Fin N) : SpinTensorIndex I degree → ℝ
  | Sum.inl _ => 0
  | Sum.inr v => amplitude v.1 * spectralTensorPlaneDerivative U I (degree v.1) σ i j v.2

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.spectralTensorPlaneDerivative

  12. lemma OAI.InvariantIsing.hasDerivAt_spinTensorFeature_plane line 153
  13. def OAI.InvariantIsing.spinTensorDerivativeCap line 162
  14. lemma OAI.InvariantIsing.spinTensorPlaneDerivative_abs_le line 167
  15. lemma OAI.InvariantIsing.measurable_spinTensorPlaneDerivative line 179
  16. def OAI.InvariantIsing.tensorNamespacedPlaneCoefficients line 189

    Source documentation

    The actual derivative coefficient map uses precisely the same Gaussian namespaces and ancestor tags as the Hamiltonian.

    def tensorNamespacedPlaneCoefficients {N m k : ℕ} (U : Orthogonal N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0)
    (i j : Fin N) (x : Spin N × LabeledLeaf n) : ℕ →₀ ℝ :=
…

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

  17. lemma OAI.InvariantIsing.hasDerivAt_tensorNamespacedCoefficient_plane line 198
  18. lemma OAI.InvariantIsing.hasDerivAt_tensorNamespacedField_plane line 212
  19. lemma OAI.InvariantIsing.measurable_tensorNamespacedPlaneCoefficient line 224
  20. def OAI.InvariantIsing.tensorNamespacedDerivativeCap line 236
  21. lemma OAI.InvariantIsing.tensorNamespacedPlaneCoefficient_abs_le line 242
  22. lemma OAI.InvariantIsing.tensorNamespacedCoefficients_mixed_cross_eq line 262

    Source documentation

    Mixed endpoint covariance is invariant under the injective change of Gaussian coordinate namespaces, not just at coinciding endpoints.

    lemma tensorNamespacedCoefficients_mixed_cross_eq {N m k : ℕ} (U V : Rotation N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0)
    (x y : Spin N × LabeledLeaf n) :
    cylinderCross (tensorNamespacedCoefficients U I degree amplitude n v x)
      (tensorNamespacedCoefficients V I degree amplitude n v y) =
    cylinderCross (tensorLeafCoefficients U I degree amplitude n v x)
      (tensorLeafCoefficients V I degree amplitude n v y) := by
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.tensorLeafCoefficients

  23. lemma OAI.InvariantIsing.hasDerivAt_tensorNamespaced_cross_plane line 283

    Source documentation

    Coefficient differentiation commutes with the finite cross covariance.

    lemma hasDerivAt_tensorNamespaced_cross_plane {N m k : ℕ} (U : Orthogonal N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0)
    (i j : Fin N) (x y : Spin N × LabeledLeaf n) :
    HasDerivAt (fun s => cylinderCross
      (tensorNamespacedCoefficients (matrixRotation (planeRotation i j s * U)) I degree amplitude n v x)
      (tensorNamespacedCoefficients (matrixRotation U) I degree amplitude n v y))
      (cylinderCross (tensorNamespacedPlaneCoefficients U I degree amplitude n v i j x)
        (tensorNamespacedCoefficients (matrixRotation U) I degree amplitude n v y)) 0 := by
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.matrixRotation, OAI.InvariantIsing.planeRotation, OAI.InvariantIsing.tensorNamespacedPlaneCoefficients

  24. lemma OAI.InvariantIsing.spinTensorFeature_mixed_rotation_cross line 307
  25. lemma OAI.InvariantIsing.tensorPrefix_weighted_sum line 334
  26. lemma OAI.InvariantIsing.tensorPrefix_linear_monomials line 344
  27. lemma OAI.InvariantIsing.tensorNamespacedPath_mixed_cross line 363

    Source documentation

    The tensor covariance at two different rotations.

    lemma tensorNamespacedPath_mixed_cross {N m k : ℕ} (U V : Rotation N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (x y : Spin N × LabeledLeaf n) :
    cylinderCross (tensorNamespacedCoefficients U I degree amplitude n
      (fun i => tensorPathProfile I degree n treeDegree h i) x)
      (tensorNamespacedCoefficients V I degree amplitude n
        (fun i => tensorPathProfile I degree n treeDegree h i) y) =
      h (labeledCommonDepth n x.2 y.2) * (∑ a, spinValue (x.1 a) * spinValue (y.1 a)) +
        ∑ r, amplitude r ^ 2 * (∏ a, mixedProjectedOverlap U V (I a) x.1 y.1 ^ degree r a) *
          treeOverlap n x.2 y.2 ^ treeDegree r := by
…

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.spinValue, OAI.InvariantIsing.mixedProjectedOverlap

  28. theorem OAI.InvariantIsing.tensorNamespacedPlaneCross_eq line 391

    Source documentation

    The coefficient derivative is exactly the one-endpoint spectral/tree covariance derivative used in the normalized Ward error estimate.

    theorem tensorNamespacedPlaneCross_eq {N m k : ℕ} (U : Orthogonal N)
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (treeDegree : Fin k → ℕ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (i j : Fin N) (x y : Spin N × LabeledLeaf n) :
    cylinderCross (tensorNamespacedPlaneCoefficients U I degree amplitude n
      (fun a => tensorPathProfile I degree n treeDegree h a) i j x)
      (tensorNamespacedCoefficients (matrixRotation U) I degree amplitude n
        (fun a => tensorPathProfile I degree n treeDegree h a) y) =
      ∑ r, amplitude r ^ 2 * treeOverlap n x.2 y.2 ^ treeDegree r *
        spectralMonomialEndpointDerivative U I (degree r) i j x.1 y.1 := by
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.tensorNamespacedPlaneCoefficients, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.matrixRotation, OAI.InvariantIsing.spectralMonomialEndpointDerivative

  29. lemma OAI.InvariantIsing.finite_tensorNamespaced_support_bound line 420

    Source documentation

    A finite spin/leaf restriction has one Gaussian coordinate prefix containing both the actual Hamiltonian coefficients and their plane derivatives, uniformly in the rotation.

    lemma finite_tensorNamespaced_support_bound {S : Type*} [Fintype S] {N m k : ℕ}
    (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
    (n : ℕ) (v : Fin (n + 1) → SpinTensorIndex I degree → ℝ≥0)
    (i j : Fin N) (x : S → Spin N × LabeledLeaf n) :
    ∃ d : ℕ,
      (∀ U : Orthogonal N, ∀ s q, q ∈ (tensorNamespacedCoefficients (matrixRotation U)
        I degree amplitude n v (x s)).support → q < d + 1) ∧
      (∀ U : Orthogonal N, ∀ s q, q ∈ (tensorNamespacedPlaneCoefficients U
        I degree amplitude n v i j (x s)).support → q < d + 1) := by
…

    Mentions: OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.Spin, OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.matrixRotation, OAI.InvariantIsing.tensorNamespacedPlaneCoefficients

  30. lemma OAI.InvariantIsing.measurable_tensorNamespacedCoefficient line 462
  31. theorem OAI.InvariantIsing.tensorNamespacedPlane_contraction_eq line 477

    Source documentation

    The exact covariance appearing after finite Gaussian integration by parts contracts to the tensor Ward error.

    theorem tensorNamespacedPlane_contraction_eq {N m : ℕ} (U : Orthogonal N)
    (I : Fin m → Finset (Fin N)) (degree : Fin N → Fin m → ℕ) (treeDegree : Fin N → ℕ)
    (n : ℕ) (u : Fin N → ℝ) (h : ℕ → ℝ) (hh : Monotone h) (h0 : 0 ≤ h 0)
    (J K : Finset (Fin N)) (η θ : Spin N) (x y : Spin N × LabeledLeaf n) :
    (N : ℝ)⁻¹ ^ 2 * ∑ i ∈ J, ∑ j ∈ K, spinCoordinate U η i * spinCoordinate U θ j *
      cylinderCross (tensorNamespacedPlaneCoefficients U I degree (tensorPerturbationAmplitude N u) n
        (fun a => tensorPathProfile I degree n treeDegree h a) i j x)
        (tensorNamespacedCoefficients (matrixRotation U) I degree (tensorPerturbationAmplitude N u) n
          (fun a => tensorPathProfile I degree n treeDegree h a) y) =
      tensorWardPerturbationError U I degree treeDegree n u J K η θ x y := by
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinCoordinate, OAI.InvariantIsing.tensorNamespacedPlaneCoefficients, OAI.InvariantIsing.tensorPerturbationAmplitude, OAI.InvariantIsing.tensorPathProfile, OAI.InvariantIsing.tensorNamespacedCoefficients, OAI.InvariantIsing.matrixRotation, OAI.InvariantIsing.tensorWardPerturbationError