BoundedMeasurableResolvent

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

The L² class of a bounded measurable datum on a bounded domain

A bounded measurable function on a bounded domain lies in L² of that domain, so the α-shifted resolvent applies to it. This file constructs the zero extension domainExtension of such a datum, records its measurability and its uniform bound, and packages the resulting L² class as boundedMeasurableToScalarL2 together with its almost-everywhere representative and the same uniform bound.

noncomputable def DivergenceFormProcess.Form.domainExtension {d : ℕ} {U : Set (HCPolySupport.Vec d)} (f : ↑U → ℝ) : HCPolySupport.Vec d → ℝ

The extension by zero of a function defined on the domain.

Equations

• DivergenceFormProcess.Form.domainExtension f = Function.extend Subtype.val f 0

@[simp]

theorem DivergenceFormProcess.Form.domainExtension_of_mem {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f : ↑U → ℝ} {x : HCPolySupport.Vec d} (hx : x ∈ U) : domainExtension f x = f ⟨x, hx⟩

theorem DivergenceFormProcess.Form.measurable_domainExtension {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) {f : ↑U → ℝ} (hf : Measurable f) : Measurable (domainExtension f)

theorem DivergenceFormProcess.Form.abs_domainExtension_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f : ↑U → ℝ} {D : ℝ} (hfD : ∀ (y : ↑U), |f y| ≤ D) (x : HCPolySupport.Vec d) : |domainExtension f x| ≤ |D|

theorem DivergenceFormProcess.Form.memScalarL2_domainExtension {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {f : ↑U → ℝ} (hfmeas : Measurable f) {D : ℝ} (hfD : ∀ (y : ↑U), |f y| ≤ D) : HCPolySupport.MemScalarL2 U (domainExtension f)

A bounded measurable function on a bounded domain lies in L² there.

noncomputable def DivergenceFormProcess.Form.boundedMeasurableToScalarL2 {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {f : ↑U → ℝ} (hfmeas : Measurable f) {D : ℝ} (hfD : ∀ (y : ↑U), |f y| ≤ D) : ↥(HCPolySupport.ScalarL2 U)

The L² class of a bounded measurable function on the domain.

Equations

• DivergenceFormProcess.Form.boundedMeasurableToScalarL2 hU hfmeas hfD = MeasureTheory.MemLp.toLp (DivergenceFormProcess.Form.domainExtension f) ⋯

theorem DivergenceFormProcess.Form.boundedMeasurableToScalarL2_coeFn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {f : ↑U → ℝ} (hfmeas : Measurable f) {D : ℝ} (hfD : ∀ (y : ↑U), |f y| ≤ D) : ↑↑(boundedMeasurableToScalarL2 hU hfmeas hfD) =ᵐ[HCPolySupport.volumeMeasureOn U] domainExtension f

theorem DivergenceFormProcess.Form.abs_boundedMeasurableToScalarL2_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {f : ↑U → ℝ} (hfmeas : Measurable f) {D : ℝ} (hfD : ∀ (y : ↑U), |f y| ≤ D) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑(boundedMeasurableToScalarL2 hU hfmeas hfD) x| ≤ |D|