Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.TestSubmodule

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.scaledClosedCubeSet_mono {d : ℕ} (Q : TriadicCube d) {ρ σ : ℝ} (hρσ : ρ ≤ σ) : scaledClosedCubeSet Q ρ ⊆ scaledClosedCubeSet Q σ

Monotonicity of concentric closed cube dilations.

theorem HCPolySupport.scaledOpenCubeSet_subset_scaledClosedCubeSet {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) : scaledOpenCubeSet Q ρ ⊆ scaledClosedCubeSet Q ρ

The open concentric subcube is contained in the corresponding closed concentric subcube.

theorem HCPolySupport.isOpen_scaledOpenCubeSet {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) : IsOpen (scaledOpenCubeSet Q ρ)

Open concentric subcubes are open subsets of the ambient Euclidean space.

theorem HCPolySupport.volume_scaledOpenCubeSet_ne_top_of_nonneg {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ : 0 ≤ ρ) : MeasureTheory.volume (scaledOpenCubeSet Q ρ) ≠ ⊤

Nonnegative scaled open subcubes have finite Lebesgue measure.

theorem HCPolySupport.euclideanCoordShift_mem_scaledClosedCubeSet_of_mem_scaledClosedCubeSet {d : ℕ} (Q : TriadicCube d) {ρ σ step : ℝ} (hρσ : ρ ≤ σ) (hstep : |step| ≤ (σ - ρ) * cubeRadius Q) (i : Fin d) {x : Vec d} (hx : x ∈ scaledClosedCubeSet Q ρ) : euclideanCoordShift step i x ∈ scaledClosedCubeSet Q σ

A small coordinate shift of a point in a smaller concentric closed cube remains in a larger concentric closed cube.

theorem HCPolySupport.scaledClosedCubeSet_subset_openCubeSet_of_nonneg_of_lt_one {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ_nonneg : 0 ≤ ρ) (hρ_lt_one : ρ < 1) : scaledClosedCubeSet Q ρ ⊆ openCubeSet Q

A concentric closed subcube with relative radius strictly below one lies in the open triadic cube.

theorem HCPolySupport.QuantitativeCubeCutoff.tsupport_subset_scaledClosedCubeSet_of_support_subset {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) : tsupport η.toFun ⊆ scaledClosedCubeSet Q ρ₂

The topological support of a quantitative cube cutoff is contained in its outer closed subcube.

theorem HCPolySupport.QuantitativeCubeCutoff.tsupport_subset_openCubeSet_of_nonneg_of_lt_one {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hρ₂_nonneg : 0 ≤ ρ₂) (hρ₂_lt_one : ρ₂ < 1) : tsupport η.toFun ⊆ openCubeSet Q

A quantitative cube cutoff whose outer radius is strictly less than one is supported inside the open triadic cube.

theorem HCPolySupport.dense_smoothCompactScalarL2 {d : ℕ} {U : Set (Vec d)} : Dense {f : ↥(ScalarL2 U) | ∃ (g : Vec d → ℝ) (hgL2 : MemScalarL2 U g), f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g}

Mathlib's global smooth compact-support density specialized to scalar L² fields on a restricted Lebesgue domain.

theorem HCPolySupport.exists_contDiff_scalarL2_tsupport_subset_eLpNorm_sub_le {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) {g : Vec d → ℝ} (hgL2 : MemScalarL2 U g) (hg_cont : ContDiff ℝ (↑⊤) g) {ε : ℝ} (hε : 0 < ε) : ∃ (φ : Vec d → ℝ) (_ : MemScalarL2 U φ), MeasureTheory.eLpNorm (g - φ) 2 (volumeMeasureOn U) ≤ ENNReal.ofReal ε ∧ ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ tsupport φ ⊆ U

Localize a smooth scalar L² field to an open finite-measure set without changing it much in L². This turns Mathlib's ambient compactly supported smooth probes into probes whose topological support is contained in U.

theorem HCPolySupport.dense_smoothCompactSupportScalarL2_tsupport_subset {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) : Dense {f : ↥(ScalarL2 U) | ∃ (g : Vec d → ℝ) (hgL2 : MemScalarL2 U g), f = MeasureTheory.MemLp.toLp g hgL2 ∧ ContDiff ℝ (↑⊤) g ∧ HasCompactSupport g ∧ tsupport g ⊆ U}

Smooth compactly supported scalar probes with support contained in an open finite-measure set are dense in L²(U).

theorem HCPolySupport.denseRange_h1WeakTestFunction_toScalarL2 {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) : DenseRange fun (φ : H1WeakTestFunction U) => φ.toScalarL2

The existing H1WeakTestFunction carrier realizes the local smooth scalar probe density as a dense range in ScalarL2.

noncomputable def HCPolySupport.H1WeakTestFunction.add {d : ℕ} {U : Set (Vec d)} (φ ψ : H1WeakTestFunction U) : H1WeakTestFunction U

Pointwise sum of two smooth weak tests on the same support set.

Equations

• φ.add ψ = { toFun := fun (z : HCPolySupport.Vec d) => φ.toFun z + ψ.toFun z, smooth := ⋯, compactSupport := ⋯, support_subset := ⋯ }

theorem HCPolySupport.H1WeakTestFunction.toScalarL2_add {d : ℕ} {U : Set (Vec d)} (φ ψ : H1WeakTestFunction U) : (φ.add ψ).toScalarL2 = φ.toScalarL2 + ψ.toScalarL2

ScalarL2 class of a pointwise sum of smooth weak tests.

noncomputable def HCPolySupport.H1WeakTestFunction.smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (φ : H1WeakTestFunction U) : H1WeakTestFunction U

Pointwise scalar multiple of a smooth weak test.

Equations

• HCPolySupport.H1WeakTestFunction.smul c φ = { toFun := fun (z : HCPolySupport.Vec d) => c • φ.toFun z, smooth := ⋯, compactSupport := ⋯, support_subset := ⋯ }

theorem HCPolySupport.H1WeakTestFunction.toScalarL2_smul {d : ℕ} {U : Set (Vec d)} (c : ℝ) (φ : H1WeakTestFunction U) : (smul c φ).toScalarL2 = c • φ.toScalarL2

ScalarL2 class of a pointwise scalar multiple of a smooth weak test.

noncomputable def HCPolySupport.h1WeakTestScalarL2Submodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ ↥(ScalarL2 U)

The scalar L² classes represented by smooth compactly supported weak tests form a submodule of ScalarL2.

Equations

• HCPolySupport.h1WeakTestScalarL2Submodule U = { carrier := Set.range fun (φ : HCPolySupport.H1WeakTestFunction U) => φ.toScalarL2, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem HCPolySupport.exists_h1WeakTestScalarL2Representative {d : ℕ} {U : Set (Vec d)} (x : ↥(h1WeakTestScalarL2Submodule U)) : ∃ (φ : H1WeakTestFunction U), φ.toScalarL2 = ↑x

noncomputable def HCPolySupport.h1WeakTestScalarL2Representative {d : ℕ} {U : Set (Vec d)} (x : ↥(h1WeakTestScalarL2Submodule U)) : H1WeakTestFunction U

A chosen smooth weak-test representative of a point in the smooth-test ScalarL2 submodule.

Equations

• HCPolySupport.h1WeakTestScalarL2Representative x = Classical.choose ⋯

theorem HCPolySupport.h1WeakTestScalarL2Representative_toScalarL2 {d : ℕ} {U : Set (Vec d)} (x : ↥(h1WeakTestScalarL2Submodule U)) : (h1WeakTestScalarL2Representative x).toScalarL2 = ↑x

The chosen representative realizes the original submodule point.

theorem HCPolySupport.dense_h1WeakTestScalarL2Submodule {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) : Dense ↑(h1WeakTestScalarL2Submodule U)

The smooth weak-test submodule is dense in scalar L² on an open finite-measure set.

theorem HCPolySupport.integral_norm_sq_sub_eq_zero_of_toScalarL2_eq {d : ℕ} {U : Set (Vec d)} {F G : Vec d → ℝ} (hF : MemScalarL2 U F) (hG : MemScalarL2 U G) (hFG : toScalarL2 hF = toScalarL2 hG) : ∫ (x : Vec d) in U, ‖F x - G x‖ ^ 2 = 0

Equality of scalar L² classes forces zero squared distance for any chosen representatives.

theorem HCPolySupport.integral_norm_sq_rpow_half_eq_norm_toScalarL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → ℝ} (hF : MemScalarL2 U F) : (∫ (x : Vec d) in U, ‖F x‖ ^ 2) ^ (1 / 2) = ‖toScalarL2 hF‖

The square-root integral norm of a scalar representative agrees with the norm of its ScalarL2 class.

theorem HCPolySupport.integral_norm_sq_rpow_half_eq_norm_h1WeakTestFunction_toScalarL2 {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) : (∫ (x : Vec d) in U, ‖φ.toFun x‖ ^ 2) ^ (1 / 2) = ‖φ.toScalarL2‖

The previous norm identification specialized to smooth weak tests.

theorem HCPolySupport.integral_norm_sq_sub_eq_zero_of_h1WeakTestFunction_toScalarL2_eq {d : ℕ} {U : Set (Vec d)} (φ ψ : H1WeakTestFunction U) (hφψ : φ.toScalarL2 = ψ.toScalarL2) : ∫ (x : Vec d) in U, ‖φ.toFun x - ψ.toFun x‖ ^ 2 = 0

Equality of the ScalarL2 classes attached to two smooth weak tests forces zero squared distance between their pointwise representatives.

noncomputable def HCPolySupport.extendH1WeakTestScalarL2Functional {d : ℕ} {U : Set (Vec d)} (ℓ : ↥(h1WeakTestScalarL2Submodule U) →ₗ[ℝ] ℝ) : ↥(ScalarL2 U) →L[ℝ] ℝ

Extend a linear functional from the smooth weak-test submodule to all of scalar L² using LinearMap.extendOfNorm. The norm estimate is supplied in the accompanying agreement and bound lemmas.

Equations

• HCPolySupport.extendH1WeakTestScalarL2Functional ℓ = ℓ.extendOfNorm (HCPolySupport.h1WeakTestScalarL2Submodule U).subtype

theorem HCPolySupport.extendH1WeakTestScalarL2Functional_apply_subtype {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) (C : ℝ) (ℓ : ↥(h1WeakTestScalarL2Submodule U) →ₗ[ℝ] ℝ) (hℓ : ∀ (x : ↥(h1WeakTestScalarL2Submodule U)), ‖ℓ x‖ ≤ C * ‖(h1WeakTestScalarL2Submodule U).subtype x‖) (x : ↥(h1WeakTestScalarL2Submodule U)) : (extendH1WeakTestScalarL2Functional ℓ) ((h1WeakTestScalarL2Submodule U).subtype x) = ℓ x

The dense-submodule extension agrees with the original functional on smooth weak-test classes.

theorem HCPolySupport.norm_extendH1WeakTestScalarL2Functional_apply_le {d : ℕ} {U : Set (Vec d)} (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) (C : ℝ) (ℓ : ↥(h1WeakTestScalarL2Submodule U) →ₗ[ℝ] ℝ) (hℓ : ∀ (x : ↥(h1WeakTestScalarL2Submodule U)), ‖ℓ x‖ ≤ C * ‖(h1WeakTestScalarL2Submodule U).subtype x‖) (x : ↥(ScalarL2 U)) : ‖(extendH1WeakTestScalarL2Functional ℓ) x‖ ≤ C * ‖x‖

The extended functional keeps the same operator bound supplied on the dense smooth-test submodule.