OAI/Geometry/RCD/Sobolev/CompactPointedTestRecovery.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.bounded_product_lipschitz line 15
2. theorem OAI.RegularPointCoordinates.compact_pointed_test_recovery_support line 35
3. theorem OAI.RegularPointCoordinates.compact_pointed_test_recovery line 90

   Source documentation

   Compactly supported smooth tests on an open ball admit harmonic recovery.

   theorem compact_pointed_test_recovery {n : ℕ} {p : X} {r S ρ a b ε B : ℝ}
       (hr : 0<r) (hρ : 0≤ρ) (hρa : ρ<a) (hab : a<b) (hbS : b<S)
       (hε : 0≤ε) (hsmall : 2*ε<a-ρ) (hB : 0≤B)
       {v : X → Euclidean n} (hv : IsPointedApproximation p 0 r S ε v)
       {ψ : Euclidean n → ℝ} {M : ℝ≥0} (hψ : LipschitzWith M ψ)
       (hψb : ∀ z, |ψ z|≤B) (hψ0 : ∀ z, ρ≤‖z‖ → ψ z=0) :
       ∃ (w : X → ℝ) (L : ℝ≥0), LipschitzWith L w ∧ HasCompactSupport w ∧
         tsupport w ⊆ ball p (S*r) ∧ (∀ x, |w x|≤B+M*ε) ∧
         r*(L:ℝ)≤M+(B+M*ε)/(b-a) ∧
         ∀ x, dist x p≤S*r → |w x-ψ (v x)|≤M*ε := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation