NormalizedDirichletError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Dimensionless Poisson value error from the actual Dirichlet energy

theorem OAI.RegularPointCoordinates.normalized_dirichlet_error line 20
Source documentation
A physical energy error of order E * r² * volume yields a squared mean value error at most C * E after division by r². This is the L2 value estimate for the genuine Poisson replacement.
```
theorem normalized_dirichlet_error (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (hvol : 0 < μ.real Ω) {r C E : ℝ} (hr : 0 < r) (hC : 0 ≤ C)
    (w : SobolevSpace μ hQ) (hw : w ∈ SobolevSpace.dirichlet μ hQ Ω)
    (hpoin : ∀ v : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ C * r ^ 2 * energyForm μ hQ v.val v.val)
    (he : ∫ x, (SobolevSpace.minimalSlope μ hQ w x) ^ 2 ∂μ ≤ E * r ^ 2 * μ.real Ω) :
    ‖normalizeLocalL2 μ Ω hfin (SobolevSpace.restrictLp μ hQ Ω ((r ^ 2)⁻¹ • w))‖ ^ 2 ≤ C * E := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp

theorem OAI.RegularPointCoordinates.normalized_dirichlet_error_tendsto_zero line 49

Source documentation

The preceding estimate tends to zero with the normalized source mass.

theorem normalized_dirichlet_error_tendsto_zero
    (Ω : ℕ → Set X) (hfin : ∀ i, μ (Ω i) ≠ ∞) (hvol : ∀ i, 0 < μ.real (Ω i))
    (r E : ℕ → ℝ) {C : ℝ} (hC : 0 ≤ C) (hr : ∀ i, 0 < r i)
    (w : ℕ → SobolevSpace μ hQ) (hw : ∀ i, w i ∈ SobolevSpace.dirichlet μ hQ (Ω i))
    (hpoin : ∀ i, ∀ v : SobolevSpace.dirichlet μ hQ (Ω i),
      ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ C * r i ^ 2 * energyForm μ hQ v.val v.val)
    (he : ∀ i, ∫ x, (SobolevSpace.minimalSlope μ hQ (w i) x) ^ 2 ∂μ ≤
      E i * r i ^ 2 * μ.real (Ω i))
    (hE : Tendsto E atTop (𝓝 0)) :
    Tendsto (fun i => ‖normalizeLocalL2 μ (Ω i) (hfin i)
      (SobolevSpace.restrictLp μ hQ (Ω i) ((r i ^ 2)⁻¹ • w i))‖) atTop (𝓝 0) := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp