ContinuousCoeffPotentialResolvent #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Potential resolvents for continuous skew coefficients #
The potential resolvent has an interior-continuous representative when
a = nu I + k and k is continuous, without a size restriction on k.
theorem
DivergenceFormProcess.Form.exists_continuousOn_representative_potentialResolvent_continuousCoeff
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
(F : ↥(HCPolySupport.ScalarL2 U))
{M : ℝ}
(hM : 0 ≤ M)
(hFM : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑F x| ≤ M)
:
∃ (v : HCPolySupport.Vec d → ℝ),
ContinuousOn v U ∧ v =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑((potentialResolvent a ⋯ hlam hEll q hq) F)
A bounded-data potential solution has a continuous representative for a continuous skew coefficient of arbitrary size.
noncomputable def
DivergenceFormProcess.Form.continuousCoeffPotentialBoundedResolvent
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hf : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
:
HCPolySupport.Vec d → ℝ
The canonical continuous representative of the bounded-data potential resolvent for an arbitrary-size continuous skew field.
Equations
- DivergenceFormProcess.Form.continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu hf hfD = Classical.choose ⋯
Instances For
theorem
DivergenceFormProcess.Form.continuousOn_continuousCoeffPotentialBoundedResolvent
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hf : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
:
ContinuousOn (continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu hf hfD) U
theorem
DivergenceFormProcess.Form.continuousCoeffPotentialBoundedResolvent_ae
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hf : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
:
continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu hf
hfD =ᵐ[HCPolySupport.volumeMeasureOn U]
↑↑((potentialResolvent a ⋯ hlam hEll q hq) (boundedMeasurableToScalarL2 hU hf hfD))
theorem
DivergenceFormProcess.Form.continuousCoeffPotentialBoundedResolvent_eq_of_continuousOn_of_ae_eq
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hf : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
{v : HCPolySupport.Vec d → ℝ}
(hv : ContinuousOn v U)
(hvae :
v =ᵐ[HCPolySupport.volumeMeasureOn U]
↑↑((potentialResolvent a ⋯ hlam hEll q hq) (boundedMeasurableToScalarL2 hU hf hfD)))
:
Set.EqOn v (continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu hf hfD) U
Characterization by continuity and the represented L² class.
theorem
DivergenceFormProcess.Form.abs_continuousCoeffPotentialBoundedResolvent_le
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[NeZero d]
(mu : ↑MarkovProcess.Semigroup.PositiveShift)
{f : ↑U → ℝ}
(hf : Measurable f)
{D : ℝ}
(hfD : ∀ (y : ↑U), |f y| ≤ D)
(x : HCPolySupport.Vec d)
:
Pointwise maximum-principle bound for the continuous potential representative.
theorem
DivergenceFormProcess.Form.continuousCoeffPotentialBoundedResolvent_add
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[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) =>
continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu hf hfD x + continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu hg hgE x)
(continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu ⋯ hfg) U
Additivity of the continuous potential representative.
theorem
DivergenceFormProcess.Form.continuousCoeffPotentialBoundedResolvent_smul
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
(a : HCPolySupport.CoeffField d)
(hU : HCPolySupport.IsOpenBoundedConvexDomain U)
{nu lam Lam C : ℝ}
(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)
(q : HCPolySupport.Vec d → ℝ)
(hq : IsBoundedNonnegativePotential U q C)
[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 * continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu hf hfD x)
(continuousCoeffPotentialBoundedResolvent a hU hnu hlam hEll hsymm hcont hd q hq mu ⋯ hcf) U
Homogeneity of the continuous potential representative.