DyadicPoissonL2Limit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Strong radial value convergence from the full dyadic source budget

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.value_error_le_normalized_mass line 19

Source documentation

A Euclidean lower volume bound converts the full-source mean-square estimate to exactly the normalized source mass already known to be summable.

theorem DyadicDistanceReplacements.value_error_le_normalized_mass
    {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C) (i : ℕ)
    {P nu : ℝ} (hP : 0 ≤ P) (hB : 0 ≤ B) (hnu : 0 < nu)
    (hvol : nu * (distanceSourceRadius r0 i) ^ (n : ℝ) ≤
      μ.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
…

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

theorem OAI.RegularPointCoordinates.DyadicDistanceReplacements.value_error_tendsto_zero line 49

Source documentation

The actual rescaled replacements converge in mean square to squared distance when the full dyadic source masses are summable.

theorem DyadicDistanceReplacements.value_error_tendsto_zero
    {n : ℕ} {κ r0 B J C : ℝ} {p : X}
    {S : DyadicDistanceSources μ hQ n κ p r0}
    (T : DyadicDistanceReplacements μ hQ S B J C)
    {P nu : ℝ} (hP : 0 ≤ P) (hB : 0 ≤ B) (hnu : 0 < nu)
    (hvol : ∀ i, nu * (distanceSourceRadius r0 i) ^ (n : ℝ) ≤
      μ.real (ball p (distanceSourceRadius r0 i)))
    (hpoin : ∀ i, ∀ 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)
    (hmass : Summable (normalizedDistanceSourceMass μ hQ S)) :
    Tendsto (fun i => ‖normalizeLocalL2 μ (ball p (distanceSourceRadius r0 i))
…