OAI/Geometry/RCD/Coordinates/NormalizedLocalL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.l2_norm_sq_eq_integral line 17
2. theorem OAI.RegularPointCoordinates.normalizeLocalL2_norm_sq line 25

   Source documentation

   This identifies the normalization with the usual mean square, including the zero-measure convention.

   theorem normalizeLocalL2_norm_sq (s : Set X) (hfin : μ s ≠ ∞)
       (f : Lp ℝ 2 (μ.restrict s)) :
       ‖normalizeLocalL2 μ s hfin f‖ ^ 2 =
         (μ.real s)⁻¹ * ∫ x in s, (f x) ^ 2 ∂μ := by
   …

   Mentions: OAI.RegularPointCoordinates.normalizeLocalL2

3. theorem OAI.RegularPointCoordinates.normalized_sobolev_mean_sq line 33
4. theorem OAI.RegularPointCoordinates.sobolev_mean_sq_le_one_of_normalized line 45

   Source documentation

   A normalized harmonic function has mean square at most one, with no pointwise value bound assumed.

   theorem sobolev_mean_sq_le_one_of_normalized (s : Set X) (hfin : μ s ≠ ∞)
       (w : SobolevSpace μ hQ)
       (h : ‖normalizeLocalL2 μ s hfin (SobolevSpace.restrictLp μ hQ s w)‖ ≤ 1) :
       (μ.real s)⁻¹ * ∫ x in s, (SobolevSpace.toLp μ hQ w x) ^ 2 ∂μ ≤ 1 := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.SobolevSpace.toLp