PartGreenH10

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

The Green potential of a bounded part domain is a zero-trace weak solution

The vanishing-shift limit partGreenPotential of the Dirichlet resolvents of a bounded measurable datum on a bounded open convex domain is identified here: it is the value function of an honest zero-trace Sobolev function on the domain solving -div (a grad w) = f weakly, with zero trace.

The representative is exact: partGreenH10 is an H10Function whose value function is partGreenPotential, not merely a function almost everywhere equal to it. Pointwise arguments downstream read the values of the Green potential, so the exact representative matters.

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

The L² class of the Green potential

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenPotentialL2 {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) : ↥(HCPolySupport.ScalarL2 V)

The L² class of the Green potential of a bounded part domain.

Equations

• A.partGreenPotentialL2 hV hf hD hfD = DivergenceFormProcess.Form.boundedMeasurableToScalarL2 hV ⋯ ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenPotentialL2_ae {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) : ↑↑(A.partGreenPotentialL2 hV hf hD hfD) =ᵐ[HCPolySupport.volumeMeasureOn V] A.partGreenPotential hV f hf hD hfD

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.norm_toL2_partShiftSolution_sub_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 : ℝ} (hlam : 0 < lam) : ‖ZeroTraceSobolev.toL2 (A.partShiftSolution hV hf hfD lam) - A.partGreenPotentialL2 hV hf hD hfD‖ ≤ scalarL2Factor V * (A.partGreenRate hV D * lam)

The L² rate of the vanishing-shift limit, from the pointwise rate.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.toL2_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.toL2 (A.partGreenSolution hV hf hD hfD) = A.partGreenPotentialL2 hV hf hD hfD

The value component of the Green solution is the L² class of the Green potential.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.toL2_partGreenSolution_ae {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.toL2 (A.partGreenSolution hV hf hD hfD)) =ᵐ[HCPolySupport.volumeMeasureOn V] A.partGreenPotential hV f hf hD hfD

The exact zero-trace representative

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_partGreenH10 {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) : ∃ (w : HCPolySupport.H10Function V), w.toFun = A.partGreenPotential hV f hf hD hfD ∧ ZeroTraceSobolev.ofH10Function w = A.partGreenSolution hV hf hD hfD

The Green potential is the value function of a zero-trace Sobolev function whose class in the carrier is the Green solution.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenH10 {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) : HCPolySupport.H10Function V

The zero-trace Sobolev function of a bounded part domain whose value function is the Green potential.

Equations

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

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.partGreenH10_toFun {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) : (A.partGreenH10 hV hf hD hfD).toFun = A.partGreenPotential hV f hf hD hfD

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.ofH10Function_partGreenH10 {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.ofH10Function (A.partGreenH10 hV hf hD hfD) = A.partGreenSolution hV hf hD hfD

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.isScalarForcedWeakSolution_partGreenH10 {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) : IsScalarForcedWeakSolution A.a V f (A.partGreenH10 hV hf hD hfD).toH1Function

The Green potential solves the unshifted zero-trace Dirichlet problem.