OAI/Geometry/RCD/Sobolev/EuclideanEulerPairing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.interior_test_mul_integrable line 14
2. theorem OAI.RegularPointCoordinates.euler_equation_of_average_pairings line 24

   Source documentation

   Separate limits of the derivative, value, constant and coordinate pairings give the weak Euler equation with the limiting coefficients.

   theorem euler_equation_of_average_pairings {n : ℕ} {S : ℝ} (hS : 0 < S)
       (w : Euclidean n → ℝ) (hw : ContDiffOn ℝ 2 w (ball 0 S))
       (ell : Euclidean n →L[ℝ] ℝ) (k : ℝ)
       (hpair : ∀ ψ : Euclidean n → ℝ, InteriorSmoothTest n S ψ →
         (volume.real (ball (0 : Euclidean n) S))⁻¹ *
             (∫ x in ball 0 S, ψ x * fderiv ℝ w x x) =
           (volume.real (ball (0 : Euclidean n) S))⁻¹ * (∫ x in ball 0 S, ψ x * w x) +
           (∑ j, ell (EuclideanSpace.single j 1) *
             ((volume.real (ball (0 : Euclidean n) S))⁻¹ * (∫ x in ball 0 S, ψ x * x j))) +
           k * ((volume.real (ball (0 : Euclidean n) S))⁻¹ * (∫ x in ball 0 S, ψ x))) :
       ∀ x ∈ ball 0 S, fderiv ℝ w x x = w x + ell x + k := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.InteriorSmoothTest