NormalizedResidualOuter.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The transport estimate in normalized local L2 spaces

theorem OAI.RegularPointCoordinates.localL2_norm_eq_root_mul_normalized line 18

theorem OAI.RegularPointCoordinates.normalized_residual_outer_bound line 28

Source documentation

The outer normalized norm is bounded uniformly from the inner one. Only a fixed four-to-one volume ratio is lost in the forcing coefficient.

theorem normalized_residual_outer_bound (n : ℕ) {F E W : ℝ}
    (hF : 0 ≤ F) (hW : 0 ≤ W) (C : ℝ≥0) :
    ∃ T : ℝ, 0 ≤ T ∧ ∀ (R a : ℝ), 0 < R → 0 ≤ a → a ≤ (n : ℝ) + 1 →
      ∀ (z : X) (f w q : SobolevSpace μ hQ) (σ : ℝ), 0 ≤ σ →
      IsConstantLaplacianOn μ hQ (ball z (4 * R)) f a →
      ∀ {B : ℝ} (hf : ∀ᵐ x ∂μ.restrict (ball z (4 * R)), localGamma μ hQ f f x ≤ B),
      (∀ᵐ x ∂μ.restrict (ball z (4 * R)), |SobolevSpace.toLp μ hQ w x| ≤ C) →
      ∀ e : X → ℝ, MemLp e 2 μ →
      localRadialDerivative μ hQ (ball z (4 * R)) f hf w =
        SobolevSpace.restrictLp μ hQ (ball z (4 * R)) (w + q) →
      localGamma μ hQ f (inwardSobolev μ hQ z (3 * R)) =ᵐ[μ.restrict (ball z (3 * R))]
        (fun x => e x - dist z x) →
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localRadialDerivative, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.inwardSobolev