PoissonEnergyError.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Energy-density error for a Poisson replacement

The linear positive-source gradient bound controls the difference of the squared gradients of the boundary datum and its Poisson replacement. This is the error paired with the Laplacian of a cutoff in the shifted Bochner mass.

theorem OAI.RegularPointCoordinates.poisson_energy_density_error_ae line 24

Source documentation

Pointwise polarization with the actual minimal weak upper gradient.

theorem poisson_energy_density_error_ae (q h : SobolevSpace μ hQ) :
    ∀ᵐ x ∂μ,
      |(1 / 2 : ℝ) * localGamma μ hQ (q - h) (q - h) x -
        (1 / 2 : ℝ) * localGamma μ hQ q q x| ≤
      SobolevSpace.minimalSlope μ hQ q x * SobolevSpace.minimalSlope μ hQ h x +
        (1 / 2 : ℝ) * (SobolevSpace.minimalSlope μ hQ h x) ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope

theorem OAI.RegularPointCoordinates.poisson_energy_density_error_le line 52

Source documentation

Integral form of the energy-density error.

theorem poisson_energy_density_error_le (Ω : Set X) (q h : SobolevSpace μ hQ)
    {A : ℝ}
    (hq : ∀ᵐ x ∂μ.restrict Ω, SobolevSpace.minimalSlope μ hQ q x ≤ A)
    (hhi : IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ h x) Ω μ) :
    (∫ x in Ω, |(1 / 2 : ℝ) * localGamma μ hQ (q - h) (q - h) x -
      (1 / 2 : ℝ) * localGamma μ hQ q q x| ∂μ) ≤
      A * (∫ x in Ω, SobolevSpace.minimalSlope μ hQ h x ∂μ) +
        (1 / 2 : ℝ) * ∫ x in Ω, (SobolevSpace.minimalSlope μ hQ h x) ^ 2 ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.localGamma

theorem OAI.RegularPointCoordinates.poisson_energy_density_error_le_source line 77

Source documentation

Linear source-mass control of the replacement's energy-density error.

theorem poisson_energy_density_error_le_source (Ω : Set X) (hΩ : MeasurableSet Ω)
    (hΩfin : μ Ω ≠ ∞) (q : SobolevSpace μ hQ) (h : SobolevSpace.dirichlet μ hQ Ω)
    (σ : Measure X) [IsFiniteMeasure σ]
    (hsource : IsDirichletMeasureSource μ hQ Ω h.val σ)
    {d C B A : ℝ} (hd : 1 < d) (hC : 0 ≤ C) (hB : 0 ≤ B) (hA : 0 ≤ A)
    (hh : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ h.val x ∧
      SobolevSpace.toLp μ hQ h.val x ≤ B)
    (hq : ∀ᵐ x ∂μ.restrict Ω, SobolevSpace.minimalSlope μ hQ q x ≤ A)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val) :
    (∫ x in Ω, |(1 / 2 : ℝ) * localGamma μ hQ (q - h.val) (q - h.val) x -
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.IsDirichletMeasureSource, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.localGamma