OAI/Geometry/EinsteinFour/ScalarLpVariation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Geometry.scalarMoment_point_derivative line 18
2. theorem OAI.PositiveEinsteinFour.Geometry.scalarMoment_derivative_bound line 28
3. theorem OAI.PositiveEinsteinFour.Geometry.scalarLpMoment_hasDerivAt line 61

   Source documentation

   A bounded measurable direction differentiates the p-moment of an arbitrary Lp function. No nonvanishing or regularity assumption is placed on the latter.

   theorem scalarLpMoment_hasDerivAt {p : ℝ} (hp : 2 < p) {f b : X → ℝ}
       (hf : MemLp f (ENNReal.ofReal p) μ) (hb : AEStronglyMeasurable b μ)
       {B : ℝ} (hB : 0 ≤ B) (hbBound : ∀ᵐ x ∂μ, |b x| ≤ B) :
       Integrable (fun x => |f x| ^ (p - 2) * f x * b x) μ ∧
         HasDerivAt (fun t : ℝ => ∫ x, |f x + t * b x| ^ p ∂μ)
           (p * ∫ x, |f x| ^ (p - 2) * f x * b x ∂μ) 0 := by
   …

4. theorem OAI.PositiveEinsteinFour.Geometry.scalarLpMoment_hasDerivAt_lp line 120

   Source documentation

   Lp-space version, ready for a weak variational equation.

   theorem scalarLpMoment_hasDerivAt_lp {p : ℝ} (hp : 2 < p)
       (f : Lp ℝ (ENNReal.ofReal p) μ) {b : X → ℝ}
       (hb : AEStronglyMeasurable b μ) {B : ℝ} (hB : 0 ≤ B)
       (hbBound : ∀ᵐ x ∂μ, |b x| ≤ B) :
       HasDerivAt (fun t : ℝ => ∫ x, |f x + t * b x| ^ p ∂μ)
         (p * ∫ x, |f x| ^ (p - 2) * f x * b x ∂μ) 0 :=
   …

5. theorem OAI.PositiveEinsteinFour.Geometry.scalarLpMoment_hasDerivAt_continuous line 130

   Source documentation

   On a compact base every continuous, hence every smooth, test direction automatically satisfies the required domination.

   theorem scalarLpMoment_hasDerivAt_continuous [TopologicalSpace X]
       [OpensMeasurableSpace X] [CompactSpace X] {p : ℝ} (hp : 2 < p)
       {f : X → ℝ} (hf : MemLp f (ENNReal.ofReal p) μ) (b : C(X, ℝ)) :
       Integrable (fun x => |f x| ^ (p - 2) * f x * b x) μ ∧
         HasDerivAt (fun t : ℝ => ∫ x, |f x + t * b x| ^ p ∂μ)
           (p * ∫ x, |f x| ^ (p - 2) * f x * b x ∂μ) 0 :=
   …