RadialHarmonicApproximation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Harmonic approximation of the actual radial derivative

theorem OAI.RegularPointCoordinates.integral_sq_sobolev_difference line 19

theorem OAI.RegularPointCoordinates.LocalHessianPairing.radial_harmonic_approximation line 31

Source documentation

Combining the Poisson energy error with weak cancellation constructs a harmonic approximation to Gamma(q,a). Its squared error is linear in the two source budgets.

theorem LocalHessianPairing.radial_harmonic_approximation
    {Ω : Set X} (hΩ : MeasurableSet Ω) (q : SobolevSpace μ hQ)
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a)
    {c P D B error : ℝ} (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (ha : IsSobolevHarmonicOn μ hQ Ω a) (b : ℝ)
    (hP : 0 ≤ P) (hD : 0 ≤ D) (hB : 0 ≤ B)
    (hgradient : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ a a x ≤ B)
    (hpoincare : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ φ.val‖ ^ 2 ≤ P * energyForm μ hQ φ.val φ.val)
    (hpoisson : (∫ x in Ω, localGamma μ hQ (q - f) (q - f) x ∂μ) ≤ error)
    (hhessian : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (G.hessian φ - b * energyForm μ hQ a φ.val) ^ 2 ≤ D * energyForm μ hQ φ.val φ.val) :
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm