LocalResidualOuterBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform residual transport using only local boundedness

theorem OAI.RegularPointCoordinates.local_uniform_residual_outer_bound line 19

Source documentation

Clipping outside the working ball preserves its Euler identity and all three local norms. The transport constant uses only the local bound.

theorem local_uniform_residual_outer_bound (n : ℕ) {F E : ℝ} (hF : 0 ≤ F)
    (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