PositiveSourceTruncation.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Truncation tests for the positive-source estimate

The clipped function belongs to the genuine Dirichlet space. Locality, including on the clipping level set, identifies its energy with the original function's energy below the level. Thus a source mass bound controls the truncated energy linearly in the level.

def OAI.RegularPointCoordinates.positiveClip line 25
Source documentation
Positive clipping, with a nonnegative upper level.
```
def positiveClip (t x : ℝ) : ℝ := min (max x 0) t
```
theorem OAI.RegularPointCoordinates.positiveClip_lipschitz line 27
theorem OAI.RegularPointCoordinates.positiveClip_zero line 30
def OAI.RegularPointCoordinates.positiveTruncation line 34
Source documentation
The actual clipped Sobolev function.
```
def positiveTruncation (H : SobolevSpace μ hQ) (t : ℝ) (ht : 0 ≤ t) : SobolevSpace μ hQ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.positiveTruncation_coe line 37
theorem OAI.RegularPointCoordinates.positiveTruncation_mem_dirichlet line 42
theorem OAI.RegularPointCoordinates.positiveTruncation_bounds line 48
theorem OAI.RegularPointCoordinates.positiveTruncation_gamma line 59
Source documentation
The energy density of the clipping, paired with the original function, vanishes on and above the level and agrees below it.
```
theorem positiveTruncation_gamma (H : SobolevSpace μ hQ)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H x)
    {t : ℝ} (ht : 0 ≤ t) :
    localGamma μ hQ H (positiveTruncation μ hQ H t ht) =ᵐ[μ]
      fun x => if SobolevSpace.toLp μ hQ H x < t then localGamma μ hQ H H x else 0 := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.positiveTruncation
theorem OAI.RegularPointCoordinates.positiveTruncation_energy line 77
Source documentation
The two energies agree exactly, so no Cauchy--Schwarz loss occurs.
```
theorem positiveTruncation_energy (H : SobolevSpace μ hQ)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H x)
    {t : ℝ} (ht : 0 ≤ t) :
    energyForm μ hQ (positiveTruncation μ hQ H t ht) (positiveTruncation μ hQ H t ht) =
      energyForm μ hQ H (positiveTruncation μ hQ H t ht) := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.positiveTruncation

theorem OAI.RegularPointCoordinates.positiveTruncation_energy_le line 98

Source documentation

For a source of mass at most P, the energy of the truncation is at most P*t. The hypothesis is its action on bounded nonnegative tests.

theorem positiveTruncation_energy_le (Ω : Set X) (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x) (P : ℝ)
    (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) :
    energyForm μ hQ (positiveTruncation μ hQ H.val t ht)
      (positiveTruncation μ hQ H.val t ht) ≤ P * t := by
…

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