WeightedToBall #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
From a weighted mass bound to a local L² bound #
The exponentially weighted mass estimate controls the square of a solution
against a weight that is bounded below on the region of interest. Dividing by
that lower bound turns the weighted statement into the plain local L²
statement consumed by the pointwise estimate.
Main results #
theorem
DivergenceFormProcess.Decay.setIntegral_sq_le_exp_mul_weighted
{d : ℕ}
{U B : Set (HCPolySupport.Vec d)}
(hBU : B ⊆ U)
(hBmeas : MeasurableSet B)
{w theta : HCPolySupport.Vec d → ℝ}
{c : ℝ}
(hthetaNonneg : ∀ (y : HCPolySupport.Vec d), 0 ≤ theta y)
(hlower : ∀ y ∈ B, 1 ≤ Real.exp c * theta y)
(hsq : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => w y ^ 2) U MeasureTheory.volume)
(hint : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => w y ^ 2 * theta y) U MeasureTheory.volume)
:
A weight bounded below on a subset converts a weighted integral bound into a plain one on that subset.
theorem
DivergenceFormProcess.Decay.setIntegral_sq_le_exp_mul_localizedWeight
{d : ℕ}
{U B : Set (HCPolySupport.Vec d)}
(hBU : B ⊆ U)
(hBmeas : MeasurableSet B)
{w eta psi : HCPolySupport.Vec d → ℝ}
{kappa t : ℝ}
(hkappa : 0 ≤ kappa)
(hetaOne : ∀ y ∈ B, 1 ≤ eta y ^ 2)
(hpsiLow : ∀ y ∈ B, t ≤ psi y)
(hsq : MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => w y ^ 2) U MeasureTheory.volume)
(hint :
MeasureTheory.IntegrableOn (fun (y : HCPolySupport.Vec d) => w y ^ 2 * (eta y ^ 2 * Real.exp (kappa * psi y) ^ 2)) U
MeasureTheory.volume)
:
The localized exponential weight of the Agmon estimate is bounded below on
any region where the localization is at least one and the phase is at least
t.