EulerOrthogonality.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean contradiction for the sharp projection

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.euler_moments line 16

Source documentation

Euler rigidity gives an exact affine identity in the same normalized L2 space in which orthogonality passes to the limit.

theorem EuclideanHarmonicModel.euler_moments {n : ℕ} {S r : ℝ}
    (w : EuclideanHarmonicModel n S) (hS : 0 < S) (hr : r ≤ S)
    (ell : Euclidean n →L[ℝ] ℝ) (k : ℝ)
    (heuler : ∀ x ∈ ball (0 : Euclidean n) S,
      fderiv ℝ w.value x x = w.value x + ell x + k) :
    ∃ (c : ℝ) (b : Fin n → ℝ),
      w.moments hr none = c • w.moments hr (some none) +
        ∑ i, b i • w.moments hr (some (some i)) := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.euler_orthogonal_norm_zero line 70

Source documentation

An Euler solution orthogonal to the affine span has zero local norm.

theorem EuclideanHarmonicModel.euler_orthogonal_norm_zero {n : ℕ} {S r : ℝ}
    (w : EuclideanHarmonicModel n S) (hS : 0 < S) (hr : r ≤ S)
    (ell : Euclidean n →L[ℝ] ℝ) (k : ℝ)
    (heuler : ∀ x ∈ ball (0 : Euclidean n) S,
      fderiv ℝ w.value x x = w.value x + ell x + k)
    (hone : ⟪w.moments hr none, w.moments hr (some none)⟫_ℝ = 0)
    (hcoords : ∀ i, ⟪w.moments hr none, w.moments hr (some (some i))⟫_ℝ = 0) :
    ⟪w.moments hr none, w.moments hr none⟫_ℝ = 0 := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.no_unit_euler_residual line 86

Source documentation

The limit of unit residuals cannot simultaneously satisfy the Euler equation and be orthogonal to the affine coordinate span.

theorem EuclideanHarmonicModel.no_unit_euler_residual {n : ℕ} {S r : ℝ}
    (w : EuclideanHarmonicModel n S) (hS : 0 < S) (hr : r ≤ S)
    (ell : Euclidean n →L[ℝ] ℝ) (k : ℝ)
    (heuler : ∀ x ∈ ball (0 : Euclidean n) S,
      fderiv ℝ w.value x x = w.value x + ell x + k)
    (hunit : ⟪w.moments hr none, w.moments hr none⟫_ℝ = 1)
    (hone : ⟪w.moments hr none, w.moments hr (some none)⟫_ℝ = 0)
    (hcoords : ∀ i, ⟪w.moments hr none, w.moments hr (some (some i))⟫_ℝ = 0) : False := by
…

Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean