OAI/Geometry/RCD/Coordinates/AffineFitPerturbation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.normalized_affineResidual_norm_le line 17
2. theorem OAI.RegularPointCoordinates.normalized_affineResidual_perturbation line 26
3. theorem OAI.RegularPointCoordinates.affineResidual_sub_affine line 40
4. theorem OAI.RegularPointCoordinates.affineProjection_harmonic_representative line 50

   Source documentation

   Every actual outer affine projection has a Sobolev representative which is harmonic wherever the columns and local constant are harmonic.

   theorem affineProjection_harmonic_representative {n : ℕ}
       (u : Fin n → SobolevSpace μ hQ) (s : Set X) (hs : μ s ≠ ∞)
       (hu : ∀ i, IsSobolevHarmonicOn μ hQ s (u i))
       (η : SobolevSpace μ hQ) (hη : IsSobolevHarmonicOn μ hQ s η)
       (hηone : SobolevSpace.restrictLp μ hQ s η = restrictedOne μ s hs)
       (f : Lp ℝ 2 (μ.restrict s)) :
       ∃ (F : SobolevSpace μ hQ) (c : ℝ) (v : Euclidean n),
         F = c • η + sobolevColumnMap μ hQ u v ∧
         IsSobolevHarmonicOn μ hQ s F ∧
         SobolevSpace.restrictLp μ hQ s F = affineProjection μ hQ u s hs f := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.restrictedOne, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.affineProjection