OAI/Geometry/RCD/Harmonic/AffineCenterBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.normalized_affineProjection_norm_le line 16
2. theorem OAI.RegularPointCoordinates.affineFit_center_bound line 27

   Source documentation

   Any coefficients of the actual fit inherit the harmonic evaluation bound and the contraction of orthogonal projection.

   theorem affineFit_center_bound {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
       (s : Set X) (hs : μ s ≠ ∞) (v : Euclidean n) {C : ℝ} (hC : 0 ≤ C)
       (heval : ∀ c a, |c + ⟪v, a⟫_ℝ| ≤
         C * ‖normalizeLocalL2 μ s hs (affineCoordinateMap μ hQ u s hs (c, a))‖)
       (f : Lp ℝ 2 (μ.restrict s)) (c : ℝ) (a : Euclidean n)
       (hfit : affineProjection μ hQ u s hs f = affineCoordinateMap μ hQ u s hs (c, a)) :
       |c + ⟪v, a⟫_ℝ| ≤ C * ‖normalizeLocalL2 μ s hs f‖ := by
   …

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

3. theorem OAI.RegularPointCoordinates.normalized_constant_norm line 40
4. theorem OAI.RegularPointCoordinates.centered_affineFit_error line 50

   Source documentation

   Subtracting the center value from a fit costs exactly its absolute value in normalized L².

   theorem centered_affineFit_error {n : ℕ} (u : Fin n → SobolevSpace μ hQ)
       (s : Set X) (hs : μ s ≠ ∞) (hs0 : μ s ≠ 0) (v : Euclidean n)
       (f : Lp ℝ 2 (μ.restrict s)) (c : ℝ) (a : Euclidean n)
       (hfit : affineProjection μ hQ u s hs f = affineCoordinateMap μ hQ u s hs (c, a)) :
       ‖normalizeLocalL2 μ s hs
         (f - affineCoordinateMap μ hQ u s hs (-⟪v, a⟫_ℝ, a))‖ ≤
         ‖normalizeLocalL2 μ s hs (affineResidual μ hQ u s hs f)‖ + |c + ⟪v, a⟫_ℝ| := by
   …

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