PositiveSourceTail.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Power tails from the actual Dirichlet truncation test

This is the Sobolev step in the positive-source estimate. The measure bound is derived from clipped moments and then applied to genuine Dirichlet functions with a bounded positive source functional.

theorem OAI.RegularPointCoordinates.power_tail_of_clip_moment line 22

Source documentation

The clipped Sobolev moment inequality implies the weak power tail.

theorem power_tail_of_clip_moment {X : Type*} [MeasurableSpace X]
    (ν : Measure X) [IsFiniteMeasure ν] {H : X → ℝ} (hH : Measurable H)
    {d C : ℝ} (hd : 0 < d) (hC : 0 ≤ C)
    (hclip : ∀ t : ℝ, 0 < t →
      (∫ x, (positiveClip t (H x)) ^ (2 * d) ∂ν) ^ (1 / d) ≤ C * t)
    {t : ℝ} (ht : 0 < t) :
    ν {x | t ≤ H x} ≤ ENNReal.ofReal (C ^ d * t ^ (-d)) := by
…

Mentions: OAI.RegularPointCoordinates.positiveClip

theorem OAI.RegularPointCoordinates.dirichlet_positive_source_tail line 72

Source documentation

The weak power tail for a positive-source Dirichlet solution. The Sobolev inequality and source bound are stated separately, on the actual Dirichlet space. The desired tail is derived rather than postulated.

theorem dirichlet_positive_source_tail (Ω : Set X) (hΩfin : μ Ω ≠ ∞)
    (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x)
    {d C P : ℝ} (hd : 0 < 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)
    {t : ℝ} (ht : 0 < t) :
    (μ.restrict Ω) {x | t ≤ SobolevSpace.toLp μ hQ H.val x} ≤
…

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