PenalizationSequence

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Exterior penalization on a nested domain

This module constructs the bounded potentials which penalize the complement of a part domain and proves the compactness estimates for their resolvents.

noncomputable def DivergenceFormProcess.Form.penalizationPotential {d : ℕ} (U V : Set (HCPolySupport.Vec d)) (n : ℕ) (x : HCPolySupport.Vec d) : ℝ

The exterior penalization potential n · 1_(U \ V).

Equations

• DivergenceFormProcess.Form.penalizationPotential U V n x = (U \ V).indicator (fun (x : HCPolySupport.Vec d) => ↑n) x

theorem DivergenceFormProcess.Form.penalizationPotential_isBoundedNonnegative {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (hV : MeasurableSet V) (n : ℕ) : IsBoundedNonnegativePotential U (penalizationPotential U V n) ↑n

The exterior penalization is a bounded nonnegative potential.

noncomputable def DivergenceFormProcess.Form.penalizedSolution {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : IsOpen U) (hV : IsOpen V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (n : ℕ) : ↥(HCPolySupport.ScalarL2 U) →L[ℝ] ZeroTraceSobolev U

The zero-trace solution of the exterior-penalized problem.

Equations

• DivergenceFormProcess.Form.penalizedSolution a hU hV hα hlam hEll n = DivergenceFormProcess.Form.potentialSolution a hα hlam hEll (DivergenceFormProcess.Form.penalizationPotential U V n) ⋯

noncomputable def DivergenceFormProcess.Form.penalizedResolvent {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : IsOpen U) (hV : IsOpen V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (n : ℕ) : ↥(HCPolySupport.ScalarL2 U) →L[ℝ] ↥(HCPolySupport.ScalarL2 U)

The scalar L² resolvent of the exterior-penalized problem.

Equations

• DivergenceFormProcess.Form.penalizedResolvent a hU hV hα hlam hEll n = DivergenceFormProcess.Form.potentialResolvent a hα hlam hEll (DivergenceFormProcess.Form.penalizationPotential U V n) ⋯

@[simp]

theorem DivergenceFormProcess.Form.penalizedResolvent_apply {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : IsOpen U) (hV : IsOpen V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (n : ℕ) (f : ↥(HCPolySupport.ScalarL2 U)) : (penalizedResolvent a hU hV hα hlam hEll n) f = ZeroTraceSobolev.toL2 ((penalizedSolution a hU hV hα hlam hEll n) f)

The penalized resolvent is the value component of the penalized solution.

theorem DivergenceFormProcess.Form.penalizationPotential_mono {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (n m : ℕ) (hnm : n ≤ m) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, penalizationPotential U V n x ≤ penalizationPotential U V m x

The exterior potentials increase with the penalization parameter.

theorem DivergenceFormProcess.Form.penalizedResolvent_antitone_ae {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) (n m : ℕ) (hnm : n ≤ m) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ↑↑((penalizedResolvent a ⋯ ⋯ hα hlam hEll m) f) x ≤ ↑↑((penalizedResolvent a ⋯ ⋯ hα hlam hEll n) f) x

Penalized resolvents of nonnegative data decrease almost everywhere as the exterior penalty increases.

theorem DivergenceFormProcess.Form.penalizedResolvent_nonneg_ae {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) (n : ℕ) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑((penalizedResolvent a ⋯ ⋯ hα hlam hEll n) f) x

Penalized resolvents of nonnegative data are nonnegative almost everywhere.

theorem DivergenceFormProcess.Form.norm_penalizedSolution_le {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : IsOpen U) (hV : IsOpen V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (n : ℕ) : ‖(penalizedSolution a hU hV hα hlam hEll n) f‖ ≤ (min α lam)⁻¹ * ‖f‖

The zero-trace graph norms of the penalized solutions have a bound independent of the penalty.

theorem DivergenceFormProcess.Form.penalized_exterior_integral_le {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : IsOpen U) (hV : IsOpen V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (n : ℕ) : ↑n * ∫ (x : HCPolySupport.Vec d) in U \ V, ↑↑((penalizedResolvent a hU hV hα hlam hEll n) f) x ^ 2 ≤ ‖f‖ * ‖(penalizedResolvent a hU hV hα hlam hEll n) f‖

The potential-energy estimate is exactly an exterior L² penalty estimate.

noncomputable def DivergenceFormProcess.Form.penalizationPointwiseLimit {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : IsOpen U) (hV : IsOpen V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : HCPolySupport.Vec d → ℝ

The pointwise infimum of the exterior-penalized resolvents.

Equations

• DivergenceFormProcess.Form.penalizationPointwiseLimit a hU hV hα hlam hEll f x = ⨅ (n : ℕ), ↑↑((DivergenceFormProcess.Form.penalizedResolvent a hU hV hα hlam hEll n) f) x

theorem DivergenceFormProcess.Form.penalizedResolvent_tendsto_pointwiseLimit_ae {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, Filter.Tendsto (fun (n : ℕ) => ↑↑((penalizedResolvent a ⋯ ⋯ hα hlam hEll n) f) x) Filter.atTop (nhds (penalizationPointwiseLimit a ⋯ ⋯ hα hlam hEll f x))

The penalized resolvents converge almost everywhere to their pointwise infimum.

theorem DivergenceFormProcess.Form.penalizationPointwiseLimit_memLp {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : MeasureTheory.MemLp (penalizationPointwiseLimit a ⋯ ⋯ hα hlam hEll f) 2 (HCPolySupport.volumeMeasureOn U)

The pointwise infimum of the penalized resolvents belongs to L²(U).

theorem DivergenceFormProcess.Form.penalizedResolvent_tendsto_L2 {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : Filter.Tendsto (fun (n : ℕ) => (penalizedResolvent a ⋯ ⋯ hα hlam hEll n) f) Filter.atTop (nhds (MeasureTheory.MemLp.toLp (penalizationPointwiseLimit a ⋯ ⋯ hα hlam hEll f) ⋯))

The monotone penalized resolvents converge strongly in L²(U) to their almost-everywhere infimum.