BoundedMeasurableAlgebra

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

Linearity of the zero extension of bounded measurable data

The zero extension of a bounded measurable function on the domain is additive and homogeneous, hence so is its L² class. These are the closure properties used by the monotone-class comparison with the process resolvent.

The zero extension is linear

theorem DivergenceFormProcess.Form.domainExtension_add_apply {d : ℕ} {U : Set (HCPolySupport.Vec d)} (f g : ↑U → ℝ) (x : HCPolySupport.Vec d) : domainExtension (fun (a : ↑U) => f a + g a) x = domainExtension f x + domainExtension g x

theorem DivergenceFormProcess.Form.domainExtension_smul_apply {d : ℕ} {U : Set (HCPolySupport.Vec d)} (c : ℝ) (f : ↑U → ℝ) (x : HCPolySupport.Vec d) : domainExtension (c • f) x = c * domainExtension f x

The L² class is linear

theorem DivergenceFormProcess.Form.boundedMeasurableToScalarL2_add {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {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) : boundedMeasurableToScalarL2 hU ⋯ hfg = boundedMeasurableToScalarL2 hU hf hfD + boundedMeasurableToScalarL2 hU hg hgE

theorem DivergenceFormProcess.Form.boundedMeasurableToScalarL2_smul {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (c : ℝ) {f : ↑U → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (y : ↑U), |f y| ≤ D) (hcf : ∀ (y : ↑U), |(c • f) y| ≤ |c| * D) : boundedMeasurableToScalarL2 hU ⋯ hcf = c • boundedMeasurableToScalarL2 hU hf hfD