ContinuousCoeffBoundedResolvent #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Bounded measurable resolvents for continuous skew coefficients #
This is the freezing-based replacement for the small-contrast representative
used by the whole-space exhaustion. It assumes a = nu I + k, with k
continuous and skew, but imposes no size bound on k.
noncomputable def
DivergenceFormProcess.Form.continuousCoeffBoundedResolvent
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{lam Lam nu : ℝ}
(hnu : 0 < nu)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
(hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1)
(hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U)
(hd : 2 ≤ d)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hfmeas : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
:
HCPolySupport.Vec d → ℝ
The representative continuous on U of a bounded measurable resolvent,
obtained by freezing the continuous skew part at each point.
Equations
- DivergenceFormProcess.Form.continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu hfmeas hfD = Classical.choose ⋯
Instances For
theorem
DivergenceFormProcess.Form.continuousOn_continuousCoeffBoundedResolvent
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{lam Lam nu : ℝ}
(hnu : 0 < nu)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
(hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1)
(hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U)
(hd : 2 ≤ d)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hfmeas : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
:
ContinuousOn (continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu hfmeas hfD) U
theorem
DivergenceFormProcess.Form.continuousCoeffBoundedResolvent_ae
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{lam Lam nu : ℝ}
(hnu : 0 < nu)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
(hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1)
(hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U)
(hd : 2 ≤ d)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hfmeas : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
:
continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu hfmeas hfD =ᵐ[HCPolySupport.volumeMeasureOn U]
↑↑((alphaShiftedResolvent a ⋯ hlam hEll) (boundedMeasurableToScalarL2 hU hfmeas hfD))
theorem
DivergenceFormProcess.Form.continuousCoeffBoundedResolvent_eq_of_continuousOn_of_ae_eq
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{lam Lam nu : ℝ}
(hnu : 0 < nu)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
(hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1)
(hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U)
(hd : 2 ≤ d)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hfmeas : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
{v : HCPolySupport.Vec d → ℝ}
(hv : ContinuousOn v U)
(hvae :
v =ᵐ[HCPolySupport.volumeMeasureOn U]
↑↑((alphaShiftedResolvent a ⋯ hlam hEll) (boundedMeasurableToScalarL2 hU hfmeas hfD)))
:
Set.EqOn v (continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu hfmeas hfD) U
The freezing representative is characterized by continuity and its
almost-everywhere L² value.
theorem
DivergenceFormProcess.Form.abs_continuousCoeffBoundedResolvent_le
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{lam Lam nu : ℝ}
(hnu : 0 < nu)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
(hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1)
(hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U)
(hd : 2 ≤ d)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hfmeas : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
(x : HCPolySupport.Vec d)
:
Pointwise maximum-principle bound for the freezing representative.
theorem
DivergenceFormProcess.Form.continuousCoeffBoundedResolvent_add
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{lam Lam nu : ℝ}
(hnu : 0 < nu)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
(hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1)
(hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U)
(hd : 2 ≤ d)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f g : ↑U → ℝ}
(hf : Measurable f)
(hg : Measurable g)
{D E : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
(hgE : ∀ (y : ↑U), |g y| ≤ E)
(hfg : ∀ (y : ↑U), |(f + g) y| ≤ D + E)
:
Set.EqOn
(fun (x : HCPolySupport.Vec d) =>
continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu hf hfD x + continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu hg hgE x)
(continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu ⋯ hfg) U
Additivity of the freezing representative on its domain.
theorem
DivergenceFormProcess.Form.continuousCoeffBoundedResolvent_smul
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{lam Lam nu : ℝ}
(hnu : 0 < nu)
(hlam : 0 < lam)
(hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a)
(hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1)
(hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U)
(hd : 2 ≤ d)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
(c : ℝ)
{f : ↑U → ℝ}
(hf : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
(hcf : ∀ (y : ↑U), |(c • f) y| ≤ |c| * D)
:
Set.EqOn
(fun (x : HCPolySupport.Vec d) => c * continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu hf hfD x)
(continuousCoeffBoundedResolvent a hU hnu hlam hEll hsymm hcont hd mu ⋯ hcf) U
Homogeneity of the freezing representative on its domain.