ResidualOuterBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform outer norm for an unnormalized projected residual

theorem OAI.RegularPointCoordinates.restrictLp_norm_sq line 18

theorem OAI.RegularPointCoordinates.residual_outer_bound line 27

Source documentation

The larger-ball bound has a constant independent of both the small inner residual norm and the source error. This is the estimate needed before dividing the residual by its norm in the compactness argument.

theorem residual_outer_bound {n : ℕ} {R a F E : ℝ} (hR : 2 ≤ R)
    (ha : 0 ≤ a) (han : a ≤ (n : ℝ) + 1) (hF : 0 ≤ F)
    (C : ℝ≥0) :
    ∃ T : ℝ, 0 ≤ T ∧ ∀ (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 ∂μ, |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 (4 * 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