ScaledForcingCoefficient.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Radius-weighted forcing coefficients before residual normalization

theorem OAI.RegularPointCoordinates.weighted_projected_euler_coefficient_bound line 19

Source documentation

The forcing coefficients are controlled by the small inner residual and its radial derivative, rather than by the full size of the projection.

theorem weighted_projected_euler_coefficient_bound {n : ℕ} (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (f w η e : SobolevSpace μ hQ) {B : ℝ}
    (hf : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ f f x ≤ B)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ.restrict Ω] fun _ => (1 : ℝ))
    (u : Fin n → SobolevSpace μ hQ) (N : Euclidean n ≃L[ℝ] Euclidean n)
    (ell : Euclidean n) (k R : ℝ) {H α Cg Cw E : ℝ} (hH : 0 ≤ H)
    (hbound : ∀ c a, |c| + R * ‖N.symm a‖ ≤ H *
      ‖normalizeLocalL2 μ Ω hfin (affineCoordinateMap μ hQ u Ω hfin (c, a))‖)
    (heuler : localRadialDerivative μ hQ Ω f hf w = SobolevSpace.restrictLp μ hQ Ω
      (w + sobolevColumnMap μ hQ u ell + k • η + e))
    (hD : ‖normalizeLocalL2 μ Ω hfin (localRadialDerivative μ hQ Ω f hf w)‖ ≤ Cg * α)
    (hw : ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω w)‖ ≤ Cw * α)
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.affineCoordinateMap, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.sobolevColumnMap

theorem OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput.scaled_forcing_coefficients line 51

Source documentation

On the half ball, the affine forcing is bounded by the original residual norm and its Euler error. This supplies the coefficients needed by radial transport without assuming their smallness.

theorem LocalHarmonicL2GradientInput.scaled_forcing_coefficients
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hinput : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n) {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (R : ℝ), 0 < R → -κ ≤ K * R ^ 2 →
      ∀ (f w η e : SobolevSpace (hausdorff n X) hX.quadratic) (B : ℝ), 0 ≤ B →
      ∀ hf : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (R / 2)),
        localGamma (hausdorff n X) hX.quadratic f f x ≤ B ^ 2,
      IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) w →
      (SobolevSpace.toLp (hausdorff n X) hX.quadratic η =ᵐ[
        (hausdorff n X).restrict (ball p (R / 2))] fun _ => (1 : ℝ)) →
      ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
        (N : Euclidean n ≃L[ℝ] Euclidean n) (ell : Euclidean n) (k H V E : ℝ),
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.weighted_affine_forcing_norm_bound line 110

Source documentation

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

theorem weighted_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 L C D α s : ℝ}
    (hR : 0 ≤ R) (hL : 0 ≤ L) (hD : 0 ≤ D) (hα : 0 ≤ α)
    (hU : ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (U ell))‖ ≤ L * (R * ‖N.symm ell‖))
    (hcoeff : |k| + R * ‖N.symm ell‖ ≤ C * (α + s))
    (he : ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω e)‖ ≤ D * s) :
    ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω (U ell + k • η + e))‖ ≤
      ((1 + L) * C + D) * (α + s) := by
…

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