DomainMaps

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

Fixed-ambient domain maps

This module places every scalar domain L² space inside the single ambient space L²(ℝᵈ).

Main definitions and results:

• AmbientScalarL2 is the fixed scalar ambient space.
• restrictToDomain restricts an ambient function to U.
• zeroExtendFromDomain is the isometric zero extension from U.
• ambientSupportProjection is their composite; it acts by the indicator of U, is idempotent and contractive, and is complementary to the projection onto Uᶜ.

@[reducible, inline]

noncomputable abbrev DivergenceFormProcess.Form.AmbientScalarL2 (d : ℕ) : AddSubgroup (HCPolySupport.Vec d →ₘ[MeasureTheory.volume] ℝ)

Scalar-valued L² on the fixed ambient space ℝᵈ.

Equations

• DivergenceFormProcess.Form.AmbientScalarL2 d = MeasureTheory.Lp ℝ 2 MeasureTheory.volume

noncomputable def DivergenceFormProcess.Form.restrictToDomain {d : ℕ} (U : Set (HCPolySupport.Vec d)) : ↥(AmbientScalarL2 d) →L[ℝ] ↥(HCPolySupport.ScalarL2 U)

Restrict an ambient L² function to a domain.

Equations

• DivergenceFormProcess.Form.restrictToDomain U = MeasureTheory.LpToLpRestrictCLM (HCPolySupport.Vec d) ℝ ℝ MeasureTheory.volume 2 U

theorem DivergenceFormProcess.Form.restrictToDomain_coeFn {d : ℕ} (U : Set (HCPolySupport.Vec d)) (f : ↥(AmbientScalarL2 d)) : ↑↑((restrictToDomain U) f) =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑f

theorem DivergenceFormProcess.Form.zeroExtendFromDomain_memLp {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (f : ↥(HCPolySupport.ScalarL2 U)) : MeasureTheory.MemLp (U.indicator fun (x : HCPolySupport.Vec d) => ↑↑f x) 2 MeasureTheory.volume

noncomputable def DivergenceFormProcess.Form.zeroExtendFromDomainLinearMap {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) : ↥(HCPolySupport.ScalarL2 U) →ₗ[ℝ] ↥(AmbientScalarL2 d)

Extension by zero from a domain as a linear map on L² classes.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DivergenceFormProcess.Form.zeroExtendFromDomain {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) : ↥(HCPolySupport.ScalarL2 U) →ₗᵢ[ℝ] ↥(AmbientScalarL2 d)

Isometric zero extension from L²(U) into ambient L²(ℝᵈ).

Equations

• DivergenceFormProcess.Form.zeroExtendFromDomain hU = { toLinearMap := DivergenceFormProcess.Form.zeroExtendFromDomainLinearMap hU, norm_map' := ⋯ }

theorem DivergenceFormProcess.Form.zeroExtendFromDomain_coeFn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (f : ↥(HCPolySupport.ScalarL2 U)) : ↑↑((zeroExtendFromDomain hU) f) =ᵐ[MeasureTheory.volume] U.indicator fun (x : HCPolySupport.Vec d) => ↑↑f x

@[simp]

theorem DivergenceFormProcess.Form.restrictToDomain_zeroExtendFromDomain {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (f : ↥(HCPolySupport.ScalarL2 U)) : (restrictToDomain U) ((zeroExtendFromDomain hU) f) = f

noncomputable def DivergenceFormProcess.Form.ambientSupportProjection {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) : ↥(AmbientScalarL2 d) →L[ℝ] ↥(AmbientScalarL2 d)

The ambient projection onto functions supported in U.

Equations

• DivergenceFormProcess.Form.ambientSupportProjection hU = (DivergenceFormProcess.Form.zeroExtendFromDomain hU).toContinuousLinearMap ∘SL DivergenceFormProcess.Form.restrictToDomain U

@[simp]

theorem DivergenceFormProcess.Form.ambientSupportProjection_idempotent {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) (f : ↥(AmbientScalarL2 d)) : (ambientSupportProjection hU) ((ambientSupportProjection hU) f) = (ambientSupportProjection hU) f