Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.SmoothPointwise

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

Pointwise smooth backward-quotient convergence

This shard isolates the classical smooth estimate used by the C.2 limit handoff: if a coordinate derivative has a global Lipschitz bound, then the backward difference quotient converges pointwise at rate O(|h|).

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_sub_coordDeriv_le_of_coordDeriv_lipschitz {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {h : ℝ} (hh : h ≠ 0) (i : Fin d) {C : ℝ} (hC : 0 ≤ C) (hLip : ∀ (z x : Vec d), ‖euclideanCoordDeriv i u z - euclideanCoordDeriv i u x‖ ≤ C * ‖z - x‖) (x : Vec d) : ‖euclideanBackwardDifferenceQuotient h i u x - euclideanCoordDeriv i u x‖ ≤ C * ‖h‖

A global Lipschitz bound on the coordinate derivative gives a pointwise O(|h|) estimate for the backward difference quotient.

theorem HCPolySupport.euclideanCoordDeriv_lipschitz_of_fderiv_bound {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i : Fin d) {C : ℝ} (hbound : ∀ (x : Vec d), ‖fderiv ℝ (fun (z : Vec d) => euclideanCoordDeriv i u z) x‖ ≤ C) (z x : Vec d) : ‖euclideanCoordDeriv i u z - euclideanCoordDeriv i u x‖ ≤ C * ‖z - x‖

A global Fréchet-derivative bound on a coordinate derivative gives the corresponding global Lipschitz bound.

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_sub_coordDeriv_le_of_fderiv_bound {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {h : ℝ} (hh : h ≠ 0) (i : Fin d) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : Vec d), ‖fderiv ℝ (fun (z : Vec d) => euclideanCoordDeriv i u z) x‖ ≤ C) (x : Vec d) : ‖euclideanBackwardDifferenceQuotient h i u x - euclideanCoordDeriv i u x‖ ≤ C * ‖h‖

Smooth backward quotients converge pointwise at rate O(|h|) when the Fréchet derivative of the coordinate derivative is globally bounded.

theorem HCPolySupport.exists_bound_fderiv_euclideanCoordDeriv_of_contDiff_hasCompactSupport {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_compact : HasCompactSupport u) (i : Fin d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖fderiv ℝ (fun (z : Vec d) => euclideanCoordDeriv i u z) x‖ ≤ C

theorem HCPolySupport.exists_backwardDifferenceQuotient_h1WeakTest_deriv_pointwise_bound {d : ℕ} {U : Set (Vec d)} (φ : H1WeakTestFunction U) (i j : Fin d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (h : ℝ), h ≠ 0 → ∀ (x : Vec d), ‖euclideanBackwardDifferenceQuotient h i (fun (y : Vec d) => φ.deriv j y) x - (fderiv ℝ (fun (y : Vec d) => φ.deriv j y) x) (basisVec i)‖ ≤ C * ‖h‖

Smooth compactly supported weak tests have a global pointwise O(|h|) backward-quotient estimate for each Hessian coordinate.

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerHessianPairingTendsto_of_smooth_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_tendsto : Filter.Tendsto stepSeq Filter.atTop (nhds 0)) (hstep_ne : ∀ (n : ℕ), stepSeq n ≠ 0) : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j

The smooth pointwise estimate closes the SmoothLimit hypothesis whenever the quotient step sequence is nonzero and tends to zero.

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerHessianPairingTendsto_of_smooth_pointwise_bound_of_step_abs {d : ℕ} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (V : Set (Vec d)) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ σ₁ ν : ℝ} (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν ≤ σ₁) (hσ₁_lt_one : σ₁ < 1) (hstep_abs : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hstep_tendsto : Filter.Tendsto stepSeq Filter.atTop (nhds 0)) (hstep_ne : ∀ (n : ℕ), stepSeq n ≠ 0) : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j

Standard closed-cube geometry supplies the domain-shift hypotheses needed by openCubeInnerHessianPairingTendsto_of_smooth_pointwise_bound.