OAI/Geometry/RCD/Coordinates/WeightedFramedProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.weighted_framed_affine_projection_coefficients line 18

   Source documentation

   Projection coefficients are bounded in the exact normalization frame; no bound for the original coordinate change or its inverse is lost.

   theorem weighted_framed_affine_projection_coefficients {n : ℕ}
       (u : Fin n → SobolevSpace μ hQ) (s : Set X) (hfin : μ s ≠ ∞)
       (N : Euclidean n ≃L[ℝ] Euclidean n) (R : ℝ) {H : ℝ} (hH : 0 ≤ H)
       (hbound : ∀ c a, |c| + R * ‖N.symm a‖ ≤ H *
         ‖normalizeLocalL2 μ s hfin (affineCoordinateMap μ hQ u s hfin (c, a))‖)
       (f : Lp ℝ 2 (μ.restrict s)) :
       ∃ (c : ℝ) (b : Euclidean n),
         affineProjection μ hQ u s hfin f = affineCoordinateMap μ hQ u s hfin (c, N b) ∧
         |c| + R * ‖b‖ ≤ H * ‖normalizeLocalL2 μ s hfin f‖ := by
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.affineCoordinateMap, OAI.RegularPointCoordinates.affineProjection

2. theorem OAI.RegularPointCoordinates.weighted_framed_harmonic_projection_residual line 40

   Source documentation

   The least-squares residual is an actual harmonic Sobolev function on the larger working set and equals the orthogonal residual on its inner projection set. Its coefficients satisfy the exact-frame value bound.

   theorem weighted_framed_harmonic_projection_residual {n : ℕ}
       (u : Fin n → SobolevSpace μ hQ) (s Ω : Set X) (hfin : μ s ≠ ∞)
       (hsΩ : s ⊆ Ω) (hΩ : MeasurableSet Ω)
       (hu : ∀ j, IsSobolevHarmonicOn μ hQ Ω (u j))
       (v η : SobolevSpace μ hQ) (hv : IsSobolevHarmonicOn μ hQ Ω v)
       (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
       (N : Euclidean n ≃L[ℝ] Euclidean n) (R : ℝ) {H : ℝ} (hH : 0 ≤ H)
       (hbound : ∀ c a, |c| + R * ‖N.symm a‖ ≤ H *
         ‖normalizeLocalL2 μ s hfin (affineCoordinateMap μ hQ u s hfin (c, a))‖) :
       ∃ (c : ℝ) (b : Euclidean n) (w : SobolevSpace μ hQ),
         w = v - (c • η + sobolevColumnMap μ hQ u (N b)) ∧
         IsSobolevHarmonicOn μ hQ Ω w ∧
   …

   Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.affineCoordinateMap, OAI.RegularPointCoordinates.sobolevColumnMap