OAI/Geometry/RCD/Harmonic/AffineEvaluation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.affineSobolev_representative line 19
2. theorem OAI.RegularPointCoordinates.affine_evaluation_of_mean_value line 39

   Source documentation

   Moser's mean-value estimate bounds affine evaluation without requiring a choice of unique affine coefficients.

   theorem affine_evaluation_of_mean_value {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
       (hmean : LocalHarmonicL2MeanValueInput hX) (hn : 2 ≤ n) {κ : ℝ} (hκ : 0 ≤ κ) :
       ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (r : ℝ), 0 < r → -κ ≤ K * r ^ 2 →
       ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (v : X → Euclidean n),
         (∀ i, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p r) (u i)) →
         ContinuousOn v (ball p r) →
         (∀ i, SobolevSpace.toLp (hausdorff n X) hX.quadratic (u i) =ᵐ[
           (hausdorff n X).restrict (ball p r)] fun x => v x i) →
         ∀ η : SobolevSpace (hausdorff n X) hX.quadratic,
           (SobolevSpace.toLp (hausdorff n X) hX.quadratic η =ᵐ[
             (hausdorff n X).restrict (ball p r)] fun _ => (1 : ℝ)) →
         ∀ (c : ℝ) (a : Euclidean n),
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp