DyadicPoissonValueError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Mean-square value error of the actual dyadic Poisson replacements

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.normalized_value_error line 19

Source documentation

The source-energy estimate and Dirichlet Poincare give the exact normalized squared-distance value error, including the full source mass.

theorem DyadicDistanceReplacements.normalized_value_error
    {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    {P : ℝ} (hP : 0 ≤ P)
    (hvol : 0 < μ.real (ball p (distanceSourceRadius r0 i)))
    (hpoin : ∀ v : SobolevSpace.dirichlet μ hQ (ball p (distanceSourceRadius r0 i)),
      ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ P * (distanceSourceRadius r0 i) ^ 2 *
        energyForm μ hQ v.val v.val) :
    ‖normalizeLocalL2 μ (ball p (distanceSourceRadius r0 i))
      (ne_of_lt ((measure_mono ball_subset_closedBall).trans_lt
        (isCompact_closedBall p _).measure_lt_top))
…

Mentions: OAI.RegularPointCoordinates.DyadicDistanceSources, OAI.RegularPointCoordinates.DyadicDistanceReplacements, OAI.RegularPointCoordinates.distanceSourceRadius, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.normalizeLocalL2