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

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

theorem HCPolySupport.tendsto_eLpNorm_sub_mul_of_eventually_eq_one_on_compacts {d : ℕ} {U : Set (Vec d)} {g : Vec d → ℝ} {η : ℕ → Vec d → ℝ} (hUopen : IsOpen U) (hUfinite : MeasureTheory.volume U ≠ ⊤) (hg : MemScalarL2 U g) (hη_nonneg : ∀ (n : ℕ) (x : Vec d), 0 ≤ η n x) (hη_le_one : ∀ (n : ℕ) (x : Vec d), η n x ≤ 1) (hη_eventually_one : ∀ (K : Set (Vec d)), IsCompact K → K ⊆ U → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, η n x = 1) (hη_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (η n) (volumeMeasureOn U)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => g x - η n x * g x) 2 (volumeMeasureOn U)) Filter.atTop (nhds 0)

If smooth cutoffs are bounded between 0 and 1 and are eventually equal to 1 on every compact subset of an open finite-measure domain, then cutting an L² function by them converges back to the original function in L².

This is the measure-regularity part of the cube boundary approximation argument. The cube geometry only has to prove the eventual-1 hypothesis for the canonical inner cutoffs.

theorem HCPolySupport.IsCompact.exists_lt_one_subset_scaledClosedCubeSet_of_subset_openCubeSet {d : ℕ} {Q : TriadicCube d} {K : Set (Vec d)} (hK : IsCompact K) (hKU : K ⊆ openCubeSet Q) : ∃ ρ < 1, K ⊆ scaledClosedCubeSet Q ρ

A compact subset of an open triadic cube is contained in a strictly smaller concentric closed cube.

theorem HCPolySupport.eventually_subset_scaledClosedCubeSet_of_tendsto_one {d : ℕ} {Q : TriadicCube d} {K : Set (Vec d)} {ρ : ℕ → ℝ} (hρ : Filter.Tendsto ρ Filter.atTop (nhds 1)) (hK : IsCompact K) (hKU : K ⊆ openCubeSet Q) : ∀ᶠ (n : ℕ) in Filter.atTop, K ⊆ scaledClosedCubeSet Q (ρ n)

If inner radii tend to 1, they eventually contain any compact subset of the open cube.

theorem HCPolySupport.QuantitativeCubeCutoff.eventually_eq_one_on_compacts_of_tendsto_inner {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℕ → ℝ} (η : (n : ℕ) → QuantitativeCubeCutoff Q (ρ₁ n) (ρ₂ n)) (hρ₁ : Filter.Tendsto ρ₁ Filter.atTop (nhds 1)) (K : Set (Vec d)) (hK : IsCompact K) (hKU : K ⊆ openCubeSet Q) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ x ∈ K, (η n).toFun x = 1

Quantitative cube cutoffs whose inner radius tends to one are eventually identically 1 on each compact subset of the open cube.

theorem HCPolySupport.QuantitativeCubeCutoff.tendsto_eLpNorm_sub_mul_of_tendsto_inner {d : ℕ} {Q : TriadicCube d} {g : Vec d → ℝ} {ρ₁ ρ₂ : ℕ → ℝ} (η : (n : ℕ) → QuantitativeCubeCutoff Q (ρ₁ n) (ρ₂ n)) (hρ₁ : Filter.Tendsto ρ₁ Filter.atTop (nhds 1)) (hg : MemScalarL2 (openCubeSet Q) g) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => g x - (η n).toFun x * g x) 2 (volumeMeasureOn (openCubeSet Q))) Filter.atTop (nhds 0)

Cutting an L² function by quantitative cube cutoffs whose inner radii tend to one converges back to the function in L²(openCubeSet Q).

theorem HCPolySupport.QuantitativeCubeCutoff.tendsto_eLpNorm_productDerivative_sub_derivative {d : ℕ} {Q : TriadicCube d} {ψ : Vec d → ℝ} {ρ₁ ρ₂ : ℕ → ℝ} (η : (n : ℕ) → QuantitativeCubeCutoff Q (ρ₁ n) (ρ₂ n)) (hρ₁ : Filter.Tendsto ρ₁ Filter.atTop (nhds 1)) (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) (i : Fin d) (hboundary : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanCoordDeriv i (η n).toFun x * ψ x) 2 (volumeMeasureOn (openCubeSet Q))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanCoordDeriv i (fun (y : Vec d) => (η n).toFun y * ψ y) x - euclideanCoordDeriv i ψ x) 2 (volumeMeasureOn (openCubeSet Q))) Filter.atTop (nhds 0)

Product-rule derivative convergence for cutoff tests, with the genuinely hard face term isolated as the boundary-error hypothesis.