AffineForcingBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The full forcing is controlled before residual normalization

theorem OAI.RegularPointCoordinates.affine_forcing_norm_bound line 18

Source documentation

The exact-frame coefficient estimate controls the forcing on the larger transport ball, including its constant and Sobolev error.

theorem affine_forcing_norm_bound {n : ℕ} (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (hpos : μ Ω ≠ 0) (η e : SobolevSpace μ hQ)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (U : Euclidean n →L[ℝ] SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (ell : Euclidean n) (k : ℝ) {R C D α s : ℝ}
    (hR : 0 ≤ R) (hD : 0 ≤ D) (hα : 0 ≤ α)
    (hU : ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (U ell))‖ ≤ R * ‖N.symm ell‖)
    (hcoeff : |k| + ‖N.symm ell‖ ≤ C * (α + s))
    (he : ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω e)‖ ≤ D * s) :
    ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (U ell + k • η + e))‖ ≤
      ((1 + R) * C + D) * (α + s) := by
…

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