UnboundedCaccioppoli.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Caccioppoli estimates for unbounded Sobolev functions

The test is the square of a compact Lipschitz cutoff times the function. The cutoff multiplication operator makes this test admissible without assuming that the function is bounded.

theorem OAI.RegularPointCoordinates.localGamma_cutoffCLM_right line 22

Source documentation

Right-hand form of the cutoff product rule.

theorem localGamma_cutoffCLM_right (f η h : SobolevSpace μ hQ)
    {v : X → ℝ} {L B : ℝ≥0} (hv : LipschitzWith L v)
    (hs : HasCompactSupport v) (hb : ∀ x, |v x| ≤ B) (hn : ∀ x, 0 ≤ v x)
    (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] v) :
    localGamma μ hQ h (SobolevSpace.cutoffCLM μ hQ hv hs hb hn f) =ᵐ[μ]
      fun x => v x*localGamma μ hQ h f x+
        SobolevSpace.toLp μ hQ f x*localGamma μ hQ h η x := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace.cutoffCLM

theorem OAI.RegularPointCoordinates.caccioppoli_cutoffCLM_energy line 36

Source documentation

The Caccioppoli bound requires a bounded cutoff gradient, but no bound on the function tested.

theorem caccioppoli_cutoffCLM_energy (u η : SobolevSpace μ hQ)
    {v : X → ℝ} {L B A : ℝ≥0} (hv : LipschitzWith L v)
    (hs : HasCompactSupport v) (hb : ∀ x, |v x| ≤ B) (hn : ∀ x, 0 ≤ v x)
    (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] v)
    (hgrad : ∀ᵐ x ∂μ, |SobolevSpace.minimalSlope μ hQ η x| ≤ A) :
    (∫ x, (SobolevSpace.toLp μ hQ η x)^2*(SobolevSpace.minimalSlope μ hQ u x)^2 ∂μ) ≤
      2*energyForm μ hQ u (SobolevSpace.cutoffCLM μ hQ hv hs hb hn
        (SobolevSpace.cutoffCLM μ hQ hv hs hb hn u))+
      4*∫ x, (SobolevSpace.toLp μ hQ u x)^2*(SobolevSpace.minimalSlope μ hQ η x)^2 ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.caccioppoli_cutoffCLM line 87

Source documentation

The zero-source specialization used in harmonic level-set iteration.

theorem caccioppoli_cutoffCLM (u η : SobolevSpace μ hQ)
    {v : X → ℝ} {L B A : ℝ≥0} (hv : LipschitzWith L v)
    (hs : HasCompactSupport v) (hb : ∀ x, |v x| ≤ B) (hn : ∀ x, 0 ≤ v x)
    (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] v)
    (hgrad : ∀ᵐ x ∂μ, |SobolevSpace.minimalSlope μ hQ η x| ≤ A)
    (hzero : energyForm μ hQ u (SobolevSpace.cutoffCLM μ hQ hv hs hb hn
      (SobolevSpace.cutoffCLM μ hQ hv hs hb hn u)) = 0) :
    (∫ x, (SobolevSpace.toLp μ hQ η x)^2*(SobolevSpace.minimalSlope μ hQ u x)^2 ∂μ) ≤
      4*∫ x, (SobolevSpace.toLp μ hQ u x)^2*(SobolevSpace.minimalSlope μ hQ η x)^2 ∂μ := by
…