OAI/Geometry/RCD/Sobolev/PhysicalProjectionEuler.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.physical_projection_euler line 20

   Source documentation

   The physical value bound and the radius-weighted affine estimate control the actual projection coefficients. Subtracting that same fit preserves harmonicity and gives a forcing of order R² * σ.

   theorem physical_projection_euler {n : ℕ}
       (u : Fin n → SobolevSpace μ hQ) (s Ω : Set X) (hfin : μ s ≠ ∞)
       (hfinΩ : μ Ω ≠ ∞) (hsΩ : s ⊆ Ω) (hΩ : MeasurableSet Ω)
       (hu : ∀ j, IsSobolevHarmonicOn μ hQ Ω (u j))
       (f v η ev : SobolevSpace μ hQ) (hv : IsSobolevHarmonicOn μ hQ Ω v)
       (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
       (N : Euclidean n ≃L[ℝ] Euclidean n) {R H V E D σ B : ℝ}
       (_hR : 0 < R) (hH : 0 ≤ H) (_hV : 0 ≤ V) (_hE : 0 ≤ E)
       (hD : 0 ≤ D) (hσ : 0 ≤ σ)
       (hbound : ∀ c a, |c| + R * ‖N.symm a‖ ≤ H *
         ‖normalizeLocalL2 μ s hfin (affineCoordinateMap μ hQ u s hfin (c, a))‖)
       (hvalue : ‖normalizeLocalL2 μ s hfin (SobolevSpace.restrictLp μ hQ s v)‖ ≤ V * R ^ 2)
   …

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