Coarse-graining support: Support.Sobolev.Foundations.EuclideanL2CZ

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

Euclidean L² Calderon-Zygmund helpers

This file starts the q = 2 Euclidean Calderon-Zygmund discharge. The main identity will be the smooth compactly supported integration-by-parts formula ‖D²u‖₂ = ‖Δu‖₂; the lemmas below package coordinate derivatives in the project's Vec d/basisVec convention and record the support and symmetry facts needed by the IBP chain.

noncomputable def HCPolySupport.euclideanCoordDeriv {d : ℕ} (i : Fin d) (u : Vec d → ℝ) : Vec d → ℝ

Coordinate derivative in the ith basisVec direction.

Equations

• HCPolySupport.euclideanCoordDeriv i u x = (fderiv ℝ u x) (HCPolySupport.basisVec i)

theorem HCPolySupport.support_euclideanCoordDeriv_subset_tsupport {d : ℕ} (i : Fin d) (u : Vec d → ℝ) : Function.support (euclideanCoordDeriv i u) ⊆ tsupport u

The pointwise support of a coordinate derivative is contained in the topological support of the original function.

theorem HCPolySupport.tsupport_euclideanCoordDeriv_subset_tsupport {d : ℕ} (i : Fin d) (u : Vec d → ℝ) : tsupport (euclideanCoordDeriv i u) ⊆ tsupport u

Coordinate differentiation does not enlarge topological support.

noncomputable def HCPolySupport.euclideanGradient {d : ℕ} (u : Vec d → ℝ) : Vec d → Vec d

Euclidean gradient expressed in the project's coordinate-vector convention.

Equations

• HCPolySupport.euclideanGradient u x i = HCPolySupport.euclideanCoordDeriv i u x

theorem HCPolySupport.contDiff_sq {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ ↑⊤ fun (x : Vec d) => u x ^ 2

Smoothness is preserved by squaring a scalar test function.

theorem HCPolySupport.hasCompactSupport_sq {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) : HasCompactSupport fun (x : Vec d) => u x ^ 2

Compact support is preserved by squaring a scalar test function.

theorem HCPolySupport.tsupport_sq_subset {d : ℕ} (u : Vec d → ℝ) : (tsupport fun (x : Vec d) => u x ^ 2) ⊆ tsupport u

Squaring a scalar test function does not enlarge topological support.

theorem HCPolySupport.euclideanCoordDeriv_sq {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i : Fin d) (x : Vec d) : euclideanCoordDeriv i (fun (y : Vec d) => u y ^ 2) x = 2 * u x * euclideanCoordDeriv i u x

Coordinate derivative of a squared scalar test function.

theorem HCPolySupport.euclideanGradient_sq {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (x : Vec d) : euclideanGradient (fun (y : Vec d) => u y ^ 2) x = fun (i : Fin d) => 2 * u x * euclideanGradient u x i

Euclidean gradient of a squared scalar test function.

theorem HCPolySupport.euclideanGradient_eq_zero_of_notMem_tsupport {d : ℕ} {u : Vec d → ℝ} {x : Vec d} (hx : x ∉ tsupport u) : euclideanGradient u x = 0

A function has zero Euclidean gradient outside its topological support.

noncomputable def HCPolySupport.euclideanCoordSecondDeriv {d : ℕ} (i j : Fin d) (u : Vec d → ℝ) : Vec d → ℝ

Coordinate second derivative, differentiating first in i and then in j.

Equations

• HCPolySupport.euclideanCoordSecondDeriv i j u x = (fderiv ℝ (HCPolySupport.euclideanCoordDeriv i u) x) (HCPolySupport.basisVec j)

theorem HCPolySupport.support_euclideanCoordSecondDeriv_subset_tsupport {d : ℕ} (i j : Fin d) (u : Vec d → ℝ) : Function.support (euclideanCoordSecondDeriv i j u) ⊆ tsupport u

The pointwise support of a coordinate second derivative is contained in the topological support of the original function.

theorem HCPolySupport.tsupport_euclideanCoordSecondDeriv_subset_tsupport {d : ℕ} (i j : Fin d) (u : Vec d → ℝ) : tsupport (euclideanCoordSecondDeriv i j u) ⊆ tsupport u

Coordinate second differentiation does not enlarge topological support.

noncomputable def HCPolySupport.euclideanCoordThirdDeriv {d : ℕ} (i j k : Fin d) (u : Vec d → ℝ) : Vec d → ℝ

Coordinate third derivative, differentiating successively in i, j, and k.

Equations

• HCPolySupport.euclideanCoordThirdDeriv i j k u x = (fderiv ℝ (HCPolySupport.euclideanCoordSecondDeriv i j u) x) (HCPolySupport.basisVec k)

noncomputable def HCPolySupport.euclideanCoordLaplacian {d : ℕ} (u : Vec d → ℝ) : Vec d → ℝ

Coordinate Laplacian, expressed as the trace of coordinate second derivatives.

Equations

• HCPolySupport.euclideanCoordLaplacian u x = ∑ i : Fin d, HCPolySupport.euclideanCoordSecondDeriv i i u x

theorem HCPolySupport.support_euclideanCoordLaplacian_subset_tsupport {d : ℕ} (u : Vec d → ℝ) : Function.support (euclideanCoordLaplacian u) ⊆ tsupport u

The pointwise support of the coordinate Laplacian is contained in the topological support of the original function.

theorem HCPolySupport.tsupport_euclideanCoordLaplacian_subset_tsupport {d : ℕ} (u : Vec d → ℝ) : tsupport (euclideanCoordLaplacian u) ⊆ tsupport u

The coordinate Laplacian does not enlarge topological support.

theorem HCPolySupport.contDiff_euclideanCoordDeriv {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i : Fin d) : ContDiff ℝ (↑⊤) (euclideanCoordDeriv i u)

theorem HCPolySupport.hasCompactSupport_euclideanCoordDeriv {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) (i : Fin d) : HasCompactSupport (euclideanCoordDeriv i u)

theorem HCPolySupport.continuous_vecNormSq_euclideanGradient_of_contDiff {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) : Continuous fun (x : Vec d) => vecNormSq (euclideanGradient u x)

The squared Euclidean gradient norm of a smooth scalar test is continuous.

theorem HCPolySupport.hasCompactSupport_vecNormSq_euclideanGradient {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) : HasCompactSupport fun (x : Vec d) => vecNormSq (euclideanGradient u x)

The squared Euclidean gradient norm of a compactly supported scalar test is compactly supported.

theorem HCPolySupport.contDiff_euclideanCoordSecondDeriv {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i j : Fin d) : ContDiff ℝ (↑⊤) (euclideanCoordSecondDeriv i j u)

theorem HCPolySupport.hasCompactSupport_euclideanCoordSecondDeriv {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) (i j : Fin d) : HasCompactSupport (euclideanCoordSecondDeriv i j u)

theorem HCPolySupport.contDiff_euclideanCoordLaplacian {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (euclideanCoordLaplacian u)

theorem HCPolySupport.hasCompactSupport_euclideanCoordLaplacian {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) : HasCompactSupport (euclideanCoordLaplacian u)

theorem HCPolySupport.euclideanCoordSecondDeriv_eq_fderiv_fderiv {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i j : Fin d) (x : Vec d) : euclideanCoordSecondDeriv i j u x = ((fderiv ℝ (fderiv ℝ u) x) (basisVec j)) (basisVec i)

theorem HCPolySupport.euclideanCoordSecondDeriv_comm {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i j : Fin d) (x : Vec d) : euclideanCoordSecondDeriv i j u x = euclideanCoordSecondDeriv j i u x

theorem HCPolySupport.euclideanCoordSecondDeriv_comm_fun {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i j : Fin d) : euclideanCoordSecondDeriv i j u = euclideanCoordSecondDeriv j i u

theorem HCPolySupport.contDiff_euclideanCoordThirdDeriv {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i j k : Fin d) : ContDiff ℝ (↑⊤) (euclideanCoordThirdDeriv i j k u)

theorem HCPolySupport.hasCompactSupport_euclideanCoordThirdDeriv {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) (i j k : Fin d) : HasCompactSupport (euclideanCoordThirdDeriv i j k u)

theorem HCPolySupport.memVectorL2_euclideanGradient_of_contDiff_hasCompactSupport {d : ℕ} {U : Set (Vec d)} {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφs : HasCompactSupport φ) : MemVectorL2 U (euclideanGradient φ)

A smooth compactly supported scalar test has an L² Euclidean gradient on any measurable restriction.

theorem HCPolySupport.euclideanCoordThirdDeriv_diag_right_comm {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i j : Fin d) (x : Vec d) : euclideanCoordThirdDeriv i j j u x = euclideanCoordThirdDeriv j j i u x

theorem HCPolySupport.integrable_mul_of_contDiff_hasCompactSupport_left {d : ℕ} {f g : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfs : HasCompactSupport f) : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) MeasureTheory.volume

theorem HCPolySupport.integrable_mul_of_contDiff_hasCompactSupport_right {d : ℕ} {f g : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hgs : HasCompactSupport g) : MeasureTheory.Integrable (fun (x : Vec d) => f x * g x) MeasureTheory.volume

theorem HCPolySupport.integral_mul_euclideanCoordDeriv_eq_neg_integral_euclideanCoordDeriv_mul {d : ℕ} {f g : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfs : HasCompactSupport f) (i : Fin d) : ∫ (x : Vec d), f x * euclideanCoordDeriv i g x = -∫ (x : Vec d), euclideanCoordDeriv i f x * g x

theorem HCPolySupport.integral_vecDot_euclideanGradient_euclideanGradient_neg_laplacian_eq_laplacian_sq {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) : ∫ (x : Vec d), vecDot (euclideanGradient u x) (euclideanGradient (fun (y : Vec d) => -euclideanCoordLaplacian u y) x) = ∫ (x : Vec d), euclideanCoordLaplacian u x ^ 2

Smooth compactly supported weak-solution test by -Δu.

For a compactly supported smooth scalar u, the weak pairing of ∇u against ∇(-Δu) is exactly the L² norm of the coordinate Laplacian. This is the integration-by-parts bridge used after the reflected weak equation supplies the test -Δu.

theorem HCPolySupport.integral_euclideanCoordSecondDeriv_sq_eq_integral_diag_mul_diag {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (i j : Fin d) : ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 = ∫ (x : Vec d), euclideanCoordSecondDeriv i i u x * euclideanCoordSecondDeriv j j u x

Fixed-component L² Hessian identity on ℝ^d for smooth compact support.

This is the componentwise integration-by-parts brick behind the q = 2 Calderon-Zygmund identity: the square of the mixed second derivative equals, after integration, the product of the two matching pure second derivatives.

theorem HCPolySupport.integral_sum_euclideanCoordSecondDeriv_sq_eq_integral_euclideanCoordLaplacian_sq {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 = ∫ (x : Vec d), euclideanCoordLaplacian u x ^ 2

Smooth compactly supported Euclidean L² Calderon-Zygmund identity in coordinate form.

The sum of squared coordinate Hessian components has the same integral as the square of the coordinate Laplacian. This is the q = 2 replacement for the Euclidean Calderon-Zygmund citation.

theorem HCPolySupport.integral_sum_euclideanCoordSecondDeriv_sq_eq_integral_forcing_mul_neg_laplacian {d : ℕ} {u f : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hweak : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∫ (x : Vec d), vecDot (euclideanGradient u x) (euclideanGradient φ x) = ∫ (x : Vec d), f x * φ x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 = ∫ (x : Vec d), f x * -euclideanCoordLaplacian u x

Smooth compactly supported weak Euclidean CZ identity.

If a smooth compactly supported u satisfies the weak equation ∫ ∇u · ∇φ = ∫ f φ against all compactly supported smooth tests, then the coordinate Hessian energy is obtained by testing with φ = -Δu. This isolates the analytic bridge still needed for nonsmooth reflected Neumann solutions: density/mollification must produce this smooth weak-equation situation.

theorem HCPolySupport.weakPoisson_hessianEnergy_eq_forcing_laplacian {d : ℕ} {U : Set (Vec d)} {u f : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ U) (hweak : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → ∫ (x : Vec d), vecDot (euclideanGradient u x) (euclideanGradient φ x) = ∫ (x : Vec d), f x * φ x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 = ∫ (x : Vec d), f x * -euclideanCoordLaplacian u x

Local-support variant of the smooth weak Euclidean CZ identity.

It is enough for the weak equation to hold against tests supported in U, provided the potential itself has topological support in U; the test -Δu is then still supported in U.

theorem HCPolySupport.integral_sum_euclideanCoordSecondDeriv_sq_le_forcing_l2_mul_laplacian_l2 {d : ℕ} {u f : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hweak : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∫ (x : Vec d), vecDot (euclideanGradient u x) (euclideanGradient φ x) = ∫ (x : Vec d), f x * φ x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ (∫ (x : Vec d), ‖f x‖ ^ 2) ^ (1 / 2) * (∫ (x : Vec d), ‖euclideanCoordLaplacian u x‖ ^ 2) ^ (1 / 2)

Smooth compactly supported Euclidean CZ estimate in Cauchy-Schwarz form.

This is the estimate produced by the weak -Δu test before cancelling the common Laplacian factor. It is the most stable form for the later density/reflection bridge, because it separates the weak-equation step from the final square-root algebra.

theorem HCPolySupport.integral_sum_euclideanCoordSecondDeriv_sq_le_forcing_l2 {d : ℕ} {u f : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hweak : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∫ (x : Vec d), vecDot (euclideanGradient u x) (euclideanGradient φ x) = ∫ (x : Vec d), f x * φ x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ ∫ (x : Vec d), ‖f x‖ ^ 2

Smooth compactly supported Euclidean L² Calderon-Zygmund estimate after cancelling the common Laplacian factor.

theorem HCPolySupport.integral_sum_euclideanCoordSecondDeriv_sq_le_forcing_l2_mul_laplacian_l2_of_tsupport_subset {d : ℕ} {U : Set (Vec d)} {u f : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ U) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hweak : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → ∫ (x : Vec d), vecDot (euclideanGradient u x) (euclideanGradient φ x) = ∫ (x : Vec d), f x * φ x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ (∫ (x : Vec d), ‖f x‖ ^ 2) ^ (1 / 2) * (∫ (x : Vec d), ‖euclideanCoordLaplacian u x‖ ^ 2) ^ (1 / 2)

Local-support variant of the smooth compactly supported Euclidean CZ estimate.

This is the Cauchy-Schwarz estimate in the exact form needed after reflection: the weak equation is required only for smooth compactly supported tests whose topological support stays in U.

theorem HCPolySupport.integral_sum_euclideanCoordSecondDeriv_sq_le_forcing_l2_of_tsupport_subset {d : ℕ} {U : Set (Vec d)} {u f : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hu_supp : HasCompactSupport u) (hu_sub : tsupport u ⊆ U) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hweak : ∀ (φ : Vec d → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → ∫ (x : Vec d), vecDot (euclideanGradient u x) (euclideanGradient φ x) = ∫ (x : Vec d), f x * φ x) : ∑ i : Fin d, ∑ j : Fin d, ∫ (x : Vec d), euclideanCoordSecondDeriv i j u x ^ 2 ≤ ∫ (x : Vec d), ‖f x‖ ^ 2

Local-support variant of the cancelled smooth compactly supported Euclidean L² Calderon-Zygmund estimate.