OAI/Geometry/EinsteinFour/ScalarLpRelativeVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

First variation along a direction dominated by the original Lp function. This covers rational truncations of a Sobolev minimizer without boundedness of the minimizer or a separate extension of its Euler equation.

  1. theorem OAI.PositiveEinsteinFour.Geometry.scalarRelativeMoment_point_derivative line 16
  2. theorem OAI.PositiveEinsteinFour.Geometry.scalarRelativeMoment_bound line 26
  3. theorem OAI.PositiveEinsteinFour.Geometry.scalarLpRelativeMoment_hasDerivAt line 65
  4. theorem OAI.PositiveEinsteinFour.Geometry.scalarLpRelativeNormSq_hasDerivAt line 117

    Source documentation

    The squared norm derivative used to test a homogeneous energy minimum with a rational truncation of the minimizer itself.

    theorem scalarLpRelativeNormSq_hasDerivAt {p : ℝ} [Fact (1 ≤ ENNReal.ofReal p)]
    (hp : 2 < p) (f b : Lp ℝ (ENNReal.ofReal p) μ) (hf : ‖f‖ = 1)
    {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ᵐ x ∂μ, |b x| ≤ B * |f x|) :
    HasDerivAt (fun t : ℝ => ‖f + t • b‖ ^ 2)
      (2 * ∫ x, |f x| ^ (p - 2) * f x * b x ∂μ) 0 := by
…