OAI/Geometry/EinsteinFour/ScalarLpNormVariation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Geometry.scalarLp_norm_eq_moment line 19

   Source documentation

   The ordinary real Lp norm as an integral of the actual representative.

   theorem scalarLp_norm_eq_moment {p : ℝ} [Fact (1 ≤ ENNReal.ofReal p)] (hp : 0 < p)
       (f : Lp ℝ (ENNReal.ofReal p) μ) :
       ‖f‖ = (∫ x, |f x| ^ p ∂μ) ^ p⁻¹ := by
   …

2. theorem OAI.PositiveEinsteinFour.Geometry.scalarLp_moment_eq_norm_rpow line 27
3. theorem OAI.PositiveEinsteinFour.Geometry.scalarLp_norm_sq_eq_moment line 33
4. theorem OAI.PositiveEinsteinFour.Geometry.scalarLp_add_smul_moment line 40
5. theorem OAI.PositiveEinsteinFour.Geometry.scalarLpNormSq_hasDerivAt line 52

   Source documentation

   At Lp norm one, the squared norm differentiates to twice the nonlinear pairing against a bounded measurable direction.

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

6. theorem OAI.PositiveEinsteinFour.Geometry.scalarLpNormSq_hasDerivAt_continuous line 74

   Source documentation

   A continuous representative of the direction is sufficient; no regularity or pointwise sign is required of the normalized Lp function.

   theorem scalarLpNormSq_hasDerivAt_continuous [TopologicalSpace X]
       [OpensMeasurableSpace X] [CompactSpace X] {p : ℝ}
       [Fact (1 ≤ ENNReal.ofReal p)] (hp : 2 < p)
       (f b : Lp ℝ (ENNReal.ofReal p) μ) (hf : ‖f‖ = 1)
       (v : C(X, ℝ)) (hb : (b : X → ℝ) =ᵐ[μ] v) :
       HasDerivAt (fun t : ℝ => ‖f + t • b‖ ^ 2)
         (2 * ∫ x, |f x| ^ (p - 2) * f x * v x ∂μ) 0 := by
   …