WeakEulerRigidity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From weak Euler limits to the Euclidean rigidity contradiction

theorem OAI.RegularPointCoordinates.euler_equation_of_test_integrals line 16

Source documentation

The weak identity supplied by convergence of gradient pairings is pointwise for the smooth Euclidean harmonic limit.

theorem euler_equation_of_test_integrals {n : ℕ} {S : ℝ} (w : Euclidean n → ℝ)
    (hw : ContDiffOn ℝ 2 w (ball 0 S)) (ell : Euclidean n →L[ℝ] ℝ) (k : ℝ)
    (htest : ∀ ψ : Euclidean n → ℝ, ContDiff ℝ ∞ ψ → HasCompactSupport ψ →
      tsupport ψ ⊆ ball 0 S →
      (∫ x in ball 0 S, ψ x * (fderiv ℝ w x x - w x - ell x - k)) = 0) :
    ∀ x ∈ ball 0 S, fderiv ℝ w x x = w x + ell x + k := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.EuclideanHarmonicModel.no_unit_weak_euler_residual line 49

Source documentation

It is enough to pass the Euler equation against interior smooth tests. The moment limits alone then contradict the positive norm.

theorem EuclideanHarmonicModel.no_unit_weak_euler_residual {n : ℕ} {S r : ℝ}
    (w : EuclideanHarmonicModel n S) (hS : 0 < S) (hr : r ≤ S)
    (ell : Euclidean n →L[ℝ] ℝ) (k : ℝ)
    (htest : ∀ ψ : Euclidean n → ℝ, ContDiff ℝ ∞ ψ → HasCompactSupport ψ →
      tsupport ψ ⊆ ball 0 S →
      (∫ x in ball 0 S, ψ x * (fderiv ℝ w.value x x - w.value x - ell x - k)) = 0)
    (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 :=
…

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