PoissonAffineTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer the distance affine fit to the Poisson radial derivative

theorem OAI.RegularPointCoordinates.LocalHessianPairing.fit_value_transfer line 19

Source documentation

The canonical Hessian pairing is the Poisson radial derivative. Replacing the true distance by its Poisson solution costs only the already proved Poisson energy error, times the coordinate gradient bound.

theorem LocalHessianPairing.fit_value_transfer {Ω : Set X}
    {f a : SobolevSpace μ hQ} (G : LocalHessianPairing μ hQ Ω f a)
    (q F : SobolevSpace μ hQ) {B error E : ℝ} (hB : 0 ≤ B)
    (ha : ∀ᵐ x ∂μ.restrict Ω, localGamma μ hQ a a x ≤ B)
    (hpoisson : (∫ x in Ω, localGamma μ hQ (q - f) (q - f) x ∂μ) ≤ error)
    (hfit : ‖radialPairingLp μ hQ Ω q a ha - SobolevSpace.restrictLp μ hQ Ω F‖ ^ 2 ≤ E) :
    ‖SobolevSpace.restrictLp μ hQ Ω (G.mixed - F)‖ ^ 2 ≤ 2 * E + 2 * B * error := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.radialPairingLp, OAI.RegularPointCoordinates.SobolevSpace.restrictLp