PartGreenLimit

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

The vanishing-shift limit of the zero-trace solutions on a bounded part domain

The Dirichlet resolvent of a bounded measurable datum on a bounded open convex domain is the value component of a zero-trace carrier element, the solution of the shifted weak equation. That carrier element converges as the shift decreases to zero, and the value component of the limit is the Green potential of PartGreenPotential.lean.

The convergence is an energy estimate. Subtracting the weak equations at two shifts and testing against the difference gives nu * ‖grad (Z_s - Z_t)‖² ≤ t ⟪Z_t, Z_s - Z_t⟫ - s ⟪Z_s, Z_s - Z_t⟫,

whose right-hand side is at most (s + t) times a constant, because the shift-uniform supremum bound of the Dirichlet resolvents bounds every Z_lam in L² uniformly in the shift. The Poincare inequality on the carrier converts the gradient estimate into a carrier-norm estimate, so the family is Cauchy as the shift decreases to zero and the carrier is complete. The limit solves the unshifted weak equation, because the term carrying the shift vanishes.

This is the statement of ExitMeanValueIdentificationLimit.lean with the exhaustion cube replaced by an arbitrary bounded open convex domain.

theorem DivergenceFormProcess.Form.partDatumL2_ae {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ↑↑(partDatumL2 hV hf hfD) =ᵐ[HCPolySupport.volumeMeasureOn V] f

The L² class of the datum agrees almost everywhere on the domain with the datum.

The shift-indexed family on the carrier

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.partShiftSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (lam : ℝ) : ZeroTraceSobolev V

The zero-trace carrier solution of the shifted Dirichlet problem of a bounded part domain, as a function of the shift; the value at a non-positive shift is zero.

Equations

• A.partShiftSolution hV hf hfD lam = if h : 0 < lam then (DivergenceFormProcess.Form.alphaShiftedSolution A.a h ⋯ ⋯) (DivergenceFormProcess.Form.partDatumL2 hV hf hfD) else 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partShiftSolution_of_pos {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) {lam : ℝ} (hlam : 0 < lam) : A.partShiftSolution hV hf hfD lam = (alphaShiftedSolution A.a hlam ⋯ ⋯) (partDatumL2 hV hf hfD)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.isAlphaShiftedWeakSolution_partShiftSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) {lam : ℝ} (hlam : 0 < lam) : IsAlphaShiftedWeakSolution A.a V lam (partDatumL2 hV hf hfD) (A.partShiftSolution hV hf hfD lam)

The shifted weak equation of the carrier family.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.toL2_partShiftSolution_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (lam : ℝ) : ↑↑(ZeroTraceSobolev.toL2 (A.partShiftSolution hV hf hfD lam)) =ᵐ[HCPolySupport.volumeMeasureOn V] A.partShiftResolvent hV f hf hfD lam

The value component of the carrier family is the shift-indexed Dirichlet resolvent.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenL2Bound {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (D : ℝ) : ℝ

The shift-uniform L² bound of the carrier family.

Equations

• A.partGreenL2Bound hV D = DivergenceFormProcess.Form.scalarL2Factor V * (D * A.partTorsionBound hV)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenL2Bound_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {D : ℝ} (hD : 0 ≤ D) : 0 ≤ A.partGreenL2Bound hV D

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.norm_toL2_partShiftSolution_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (lam : ℝ) : ‖ZeroTraceSobolev.toL2 (A.partShiftSolution hV hf hfD lam)‖ ≤ A.partGreenL2Bound hV D

The energy estimate for two shifts

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.nu_mul_norm_gradient_partShiftSolution_sub_sq_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) : A.nu * ‖ZeroTraceSobolev.gradient (A.partShiftSolution hV hf hfD s - A.partShiftSolution hV hf hfD t)‖ ^ 2 ≤ (s + t) * (2 * A.partGreenL2Bound hV D ^ 2)

The energy of the difference of two shifts is controlled by the sum of the shifts. Subtracting the two weak equations and testing against the difference leaves only the two mass terms, each carrying an explicit factor of its shift against the shift-uniform L² bound.

The vanishing-shift limit

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_tendsto_partShiftSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ∃ (Z : ZeroTraceSobolev V), Filter.Tendsto (fun (n : ℕ) => A.partShiftSolution hV hf hfD (↑n + 1)⁻¹) Filter.atTop (nhds Z)

The carrier family is Cauchy as the shift decreases to zero and therefore converges.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : ZeroTraceSobolev V

The Green solution on the zero-trace carrier of a bounded part domain: the vanishing-shift limit of the carrier solutions of the shifted Dirichlet problem.

Equations

• A.partGreenSolution hV hf hD hfD = Classical.choose ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.tendsto_partShiftSolution_partGreenSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : Filter.Tendsto (fun (n : ℕ) => A.partShiftSolution hV hf hfD (↑n + 1)⁻¹) Filter.atTop (nhds (A.partGreenSolution hV hf hD hfD))

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.isAlphaShiftedWeakSolution_partGreenSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) : IsAlphaShiftedWeakSolution A.a V 0 (partDatumL2 hV hf hfD) (A.partGreenSolution hV hf hD hfD)

The Green solution solves the unshifted zero-trace weak equation.