PositiveSourceGradient.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Weighted gradient estimates for positive Poisson sources

The Cauchy--Schwarz step uses a reciprocal-weight energy and the moment obtained from truncation. This keeps the linear dependence on source mass which ordinary unweighted energy Cauchy--Schwarz would lose.

theorem OAI.RegularPointCoordinates.integral_sq_le_reciprocal_weight line 22

Source documentation

Weighted Cauchy--Schwarz, including the integrability conclusion.

theorem integral_sq_le_reciprocal_weight {X : Type*} [MeasurableSpace X]
    (μ : Measure X) {f w : X → ℝ} (hf : AEMeasurable f μ) (hw : AEMeasurable w μ)
    (hwpos : ∀ᵐ x ∂μ, 0 < w x)
    (hiw : Integrable w μ) (hif : Integrable (fun x => f x ^ 2 / w x) μ) :
    Integrable f μ ∧ (∫ x, f x ∂μ) ^ 2 ≤ (∫ x, f x ^ 2 / w x ∂μ) * ∫ x, w x ∂μ := by
…

theorem OAI.RegularPointCoordinates.shifted_moment_le line 70

Source documentation

Shifting a nonnegative function by one preserves controlled moments.

theorem shifted_moment_le {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ] {H : X → ℝ}
    (hH : AEMeasurable H μ) (hH0 : 0 ≤ᵐ[μ] H) {q : ℝ} (hq : 0 ≤ q)
    (hi : Integrable (fun x => H x ^ q) μ) :
    Integrable (fun x => (1 + H x) ^ q) μ ∧
      (∫ x, (1 + H x) ^ q ∂μ) ≤ 2 ^ q * (μ.real univ + ∫ x, H x ^ q ∂μ) := by
…

def OAI.RegularPointCoordinates.positiveSourceGradientBound line 103
Source documentation
An explicit, nonoptimal uniform constant for the normalized source.
```
def positiveSourceGradientBound (V C d q : ℝ) : ℝ :=
…
```

theorem OAI.RegularPointCoordinates.normalized_positive_source_gradient line 111

Source documentation

The complete normalized positive-source L1 gradient estimate from the Dirichlet Sobolev inequality and the source's action on bounded tests.

theorem normalized_positive_source_gradient (Ω : Set X) (hΩfin : μ Ω ≠ ∞)
    (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x)
    {d q C : ℝ} (hq : 1 < q) (hqd : q < d) (hC : 0 ≤ C)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ s : ℝ, 0 ≤ s →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ s) →
      energyForm μ hQ H.val φ.val ≤ s) :
    IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ H.val x) Ω μ ∧
      (∫ x in Ω, SobolevSpace.minimalSlope μ hQ H.val x ∂μ) ≤
…

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

theorem OAI.RegularPointCoordinates.positive_source_gradient_of_pos line 176

Source documentation

Scaling the normalized estimate gives linear dependence on a positive source mass.

theorem positive_source_gradient_of_pos (Ω : Set X) (hΩfin : μ Ω ≠ ∞)
    (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x)
    {d q C P : ℝ} (hq : 1 < q) (hqd : q < d) (hC : 0 ≤ C) (hP : 0 < P)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ s : ℝ, 0 ≤ s →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ s) →
      energyForm μ hQ H.val φ.val ≤ P * s) :
    IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ H.val x) Ω μ ∧
      (∫ x in Ω, SobolevSpace.minimalSlope μ hQ H.val x ∂μ) ≤
…

theorem OAI.RegularPointCoordinates.positive_source_gradient line 223

Source documentation

The linear gradient estimate also holds at zero source mass, by approaching that mass through positive upper bounds.

theorem positive_source_gradient (Ω : Set X) (hΩfin : μ Ω ≠ ∞)
    (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x)
    {d q C P : ℝ} (hq : 1 < q) (hqd : q < d) (hC : 0 ≤ C) (hP : 0 ≤ P)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ s : ℝ, 0 ≤ s →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ s) →
      energyForm μ hQ H.val φ.val ≤ P * s) :
    IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ H.val x) Ω μ ∧
      (∫ x in Ω, SobolevSpace.minimalSlope μ hQ H.val x ∂μ) ≤
…

theorem OAI.RegularPointCoordinates.positive_source_energy line 254

Source documentation

The companion square-gradient bound is the direct test by the bounded solution itself.

theorem positive_source_energy (Ω : Set X) (H : SobolevSpace.dirichlet μ hQ Ω)
    {P B : ℝ} (hB : 0 ≤ B)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x ∧ SobolevSpace.toLp μ hQ H.val x ≤ B)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ s : ℝ, 0 ≤ s →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ s) →
      energyForm μ hQ H.val φ.val ≤ P * s) :
    (∫ x, (SobolevSpace.minimalSlope μ hQ H.val x) ^ 2 ∂μ) ≤ P * B := by
…

theorem OAI.RegularPointCoordinates.positive_source_bounds line 270

Source documentation

Both positive-source estimates, with a fixed exponent selected from d > 1. The L1 bound is linear in mass; the L2 energy bound is mass times the upper bound of the solution.

theorem positive_source_bounds (Ω : Set X) (hΩfin : μ Ω ≠ ∞)
    (H : SobolevSpace.dirichlet μ hQ Ω)
    {d C P B : ℝ} (hd : 1 < d) (hC : 0 ≤ C) (hP : 0 ≤ P) (hB : 0 ≤ B)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x ∧ SobolevSpace.toLp μ hQ H.val x ≤ B)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ s : ℝ, 0 ≤ s →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ s) →
      energyForm μ hQ H.val φ.val ≤ P * s) :
    IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ H.val x) Ω μ ∧
      (∫ x in Ω, SobolevSpace.minimalSlope μ hQ H.val x ∂μ) ≤
…