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

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

theorem HCPolySupport.inner_toScalarL2_eq_integral_mul {d : ℕ} {U : Set (Vec d)} {F G : Vec d → ℝ} (hF : MemScalarL2 U F) (hG : MemScalarL2 U G) : inner ℝ (toScalarL2 hF) (toScalarL2 hG) = ∫ (x : Vec d) in U, F x * G x

Pairing representatives in scalar L² agrees with the set integral of the pointwise product.

theorem HCPolySupport.tendsto_integral_mul_of_tendsto_toScalarL2 {d : ℕ} {U : Set (Vec d)} {ι : Type u_1} {l : Filter ι} {u : Vec d → ℝ} {F : ι → Vec d → ℝ} {G : Vec d → ℝ} (hu : MemScalarL2 U u) (hF : ∀ (n : ι), MemScalarL2 U (F n)) (hG : MemScalarL2 U G) (hconv : Filter.Tendsto (fun (n : ι) => toScalarL2 ⋯) l (nhds (toScalarL2 hG))) : Filter.Tendsto (fun (n : ι) => ∫ (x : Vec d) in U, u x * F n x) l (nhds (∫ (x : Vec d) in U, u x * G x))

A fixed L² factor defines a continuous functional against convergent scalar L² representatives.

theorem HCPolySupport.tendsto_toScalarL2_of_tendsto_eLpNorm {d : ℕ} {U : Set (Vec d)} {ι : Type u_1} {l : Filter ι} {F : ι → Vec d → ℝ} {G : Vec d → ℝ} (hF : ∀ (n : ι), MemScalarL2 U (F n)) (hG : MemScalarL2 U G) (hlim : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (fun (x : Vec d) => F n x - G x) 2 (volumeMeasureOn U)) l (nhds 0)) : Filter.Tendsto (fun (n : ι) => toScalarL2 ⋯) l (nhds (toScalarL2 hG))

Raw eLpNorm convergence of representatives implies convergence of their scalar L² classes.

theorem HCPolySupport.tendsto_eLpNorm_of_tendsto_toScalarL2 {d : ℕ} {U : Set (Vec d)} {ι : Type u_1} {l : Filter ι} {F : ι → Vec d → ℝ} {G : Vec d → ℝ} (hF : ∀ (n : ι), MemScalarL2 U (F n)) (hG : MemScalarL2 U G) (hconv : Filter.Tendsto (fun (n : ι) => toScalarL2 ⋯) l (nhds (toScalarL2 hG))) : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (fun (x : Vec d) => F n x - G x) 2 (volumeMeasureOn U)) l (nhds 0)

Convergence in scalar L² of explicit representatives implies raw eLpNorm convergence of their pointwise differences.

theorem HCPolySupport.tendsto_eLpNorm_zero_of_ae_norm_le_mul_norm {d : ℕ} {U : Set (Vec d)} {F : ℕ → Vec d → ℝ} {stepSeq : ℕ → ℝ} {C : ℝ} (hUfinite : (volumeMeasureOn U) Set.univ ≠ ⊤) (hstep : Filter.Tendsto stepSeq Filter.atTop (nhds 0)) (hbound : ∀ (n : ℕ), ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, ‖F n x‖ ≤ C * ‖stepSeq n‖) (hF_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) (volumeMeasureOn U)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n) 2 (volumeMeasureOn U)) Filter.atTop (nhds 0)

On a finite-measure set, an O(|h_n|) pointwise bound forces the L² seminorm to vanish when h_n -> 0.

theorem HCPolySupport.WeakPoissonEquationOn.memScalarL2_euclideanBackwardDifferenceQuotient_h1WeakTest_deriv {d : ℕ} {S U : Set (Vec d)} {step : ℝ} (φ : H1WeakTestFunction S) (i j : Fin d) : MemScalarL2 U (euclideanBackwardDifferenceQuotient step i fun (y : Vec d) => φ.deriv j y)

Smooth test derivatives have L² backward difference quotients on any restricted ambient set.

theorem HCPolySupport.WeakPoissonEquationOn.memScalarL2_fderiv_h1WeakTest_deriv_apply {d : ℕ} {S U : Set (Vec d)} (φ : H1WeakTestFunction S) (i j : Fin d) : MemScalarL2 U fun (x : Vec d) => (fderiv ℝ (fun (y : Vec d) => φ.deriv j y) x) (basisVec i)

The classical second derivative of a smooth weak test is scalar L² on any restricted ambient set.

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerHessianPairingTendsto_of_backwardDifferenceQuotient_deriv_toScalarL2_tendsto {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ : ℝ} (hSV : scaledOpenCubeSet Q ρ₁ ⊆ V) (hVU : V ⊆ openCubeSet Q) (hVshift : ∀ (n : ℕ), ∀ x ∈ V, euclideanCoordShift (stepSeq n) i x ∈ openCubeSet Q) (hback_l2 : ∀ (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)), Filter.Tendsto (fun (n : ℕ) => toScalarL2 ⋯) Filter.atTop (nhds (toScalarL2 ⋯))) : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j

L² convergence of the smooth backward quotients is enough to close the open-inner Hessian pairing limit. The remaining analytic input is now exactly the classical statement that, for smooth compactly supported φ, D_i^- (∂_j φ) → ∂_i∂_j φ in L²(openCubeSet Q).

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerHessianPairingTendsto_of_backwardDifferenceQuotient_deriv_eLpNorm_tendsto {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ : ℝ} (hSV : scaledOpenCubeSet Q ρ₁ ⊆ V) (hVU : V ⊆ openCubeSet Q) (hVshift : ∀ (n : ℕ), ∀ x ∈ V, euclideanCoordShift (stepSeq n) i x ∈ openCubeSet Q) (hback_eLp : ∀ (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanBackwardDifferenceQuotient (stepSeq n) i (fun (y : Vec d) => φ.deriv j y) x - (fderiv ℝ (fun (y : Vec d) => φ.deriv j y) x) (basisVec i)) 2 (volumeMeasureOn (openCubeSet Q))) Filter.atTop (nhds 0)) : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j

Raw L² seminorm convergence of the smooth backward quotients is enough to close the open-inner Hessian pairing limit.

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerHessianPairingTendsto_of_backwardDifferenceQuotient_deriv_pointwise_bound {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ : ℝ} (hSV : scaledOpenCubeSet Q ρ₁ ⊆ V) (hVU : V ⊆ openCubeSet Q) (hVshift : ∀ (n : ℕ), ∀ x ∈ V, euclideanCoordShift (stepSeq n) i x ∈ openCubeSet Q) (hstep : Filter.Tendsto stepSeq Filter.atTop (nhds 0)) (hpoint : ∀ (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)), ∃ (C : ℝ), ∀ (n : ℕ), ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet Q), ‖euclideanBackwardDifferenceQuotient (stepSeq n) i (fun (y : Vec d) => φ.deriv j y) x - (fderiv ℝ (fun (y : Vec d) => φ.deriv j y) x) (basisVec i)‖ ≤ C * ‖stepSeq n‖) : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j

A pointwise mean-value type bound for the smooth quotient error closes the open-inner Hessian pairing limit. This is the intended consumer of the remaining smooth calculus estimate.