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

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

Coordinate difference quotients

This file starts the difference-quotient API needed for the interior H2 regularity proof in the cube Neumann Calderon-Zygmund discharge. The first slice is intentionally small: coordinate shifts, forward/backward quotients, and the smooth/support facts that make the eventual difference-quotient tests admissible.

def HCPolySupport.euclideanCoordShift {d : ℕ} (h : ℝ) (i : Fin d) (x : Vec d) : Vec d

Shift a point by h in coordinate direction i.

Equations

• HCPolySupport.euclideanCoordShift h i x = x + h • HCPolySupport.basisVec i

@[simp]

theorem HCPolySupport.euclideanCoordShift_apply {d : ℕ} (h : ℝ) (i : Fin d) (x : Vec d) : euclideanCoordShift h i x = x + h • basisVec i

theorem HCPolySupport.euclideanCoordShift_zero {d : ℕ} (i : Fin d) (x : Vec d) : euclideanCoordShift 0 i x = x

theorem HCPolySupport.euclideanCoordShift_zero_step {d : ℕ} (h : ℝ) (i : Fin d) : euclideanCoordShift h i 0 = h • basisVec i

theorem HCPolySupport.euclideanCoordShift_neg_cancel {d : ℕ} (h : ℝ) (i : Fin d) (x : Vec d) : euclideanCoordShift (-h) i (euclideanCoordShift h i x) = x

theorem HCPolySupport.euclideanCoordShift_cancel_neg {d : ℕ} (h : ℝ) (i : Fin d) (x : Vec d) : euclideanCoordShift h i (euclideanCoordShift (-h) i x) = x

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

Forward coordinate difference quotient.

Equations

• HCPolySupport.euclideanForwardDifferenceQuotient h i u x = (u (HCPolySupport.euclideanCoordShift h i x) - u x) / h

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

Backward coordinate difference quotient.

Equations

• HCPolySupport.euclideanBackwardDifferenceQuotient h i u x = (u x - u (HCPolySupport.euclideanCoordShift (-h) i x)) / h

@[simp]

theorem HCPolySupport.euclideanForwardDifferenceQuotient_apply {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanForwardDifferenceQuotient h i u x = (u (euclideanCoordShift h i x) - u x) / h

@[simp]

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_apply {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanBackwardDifferenceQuotient h i u x = (u x - u (euclideanCoordShift (-h) i x)) / h

theorem HCPolySupport.euclideanForwardDifferenceQuotient_mul {d : ℕ} (h : ℝ) (i : Fin d) (u v : Vec d → ℝ) (x : Vec d) : euclideanForwardDifferenceQuotient h i (fun (y : Vec d) => u y * v y) x = euclideanForwardDifferenceQuotient h i u x * v (euclideanCoordShift h i x) + u x * euclideanForwardDifferenceQuotient h i v x

Product rule for forward coordinate difference quotients.

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_mul {d : ℕ} (h : ℝ) (i : Fin d) (u v : Vec d → ℝ) (x : Vec d) : euclideanBackwardDifferenceQuotient h i (fun (y : Vec d) => u y * v y) x = euclideanBackwardDifferenceQuotient h i u x * v x + u (euclideanCoordShift (-h) i x) * euclideanBackwardDifferenceQuotient h i v x

Product rule for backward coordinate difference quotients.

theorem HCPolySupport.euclideanForwardDifferenceQuotient_sq {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanForwardDifferenceQuotient h i (fun (y : Vec d) => u y ^ 2) x = euclideanForwardDifferenceQuotient h i u x * (u (euclideanCoordShift h i x) + u x)

Square rule for forward coordinate difference quotients.

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_sq {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanBackwardDifferenceQuotient h i (fun (y : Vec d) => u y ^ 2) x = euclideanBackwardDifferenceQuotient h i u x * (u x + u (euclideanCoordShift (-h) i x))

Square rule for backward coordinate difference quotients.

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_coordShift_eq_forward {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanBackwardDifferenceQuotient h i u (euclideanCoordShift h i x) = euclideanForwardDifferenceQuotient h i u x

A backward quotient at the forward-shifted point is the corresponding forward quotient. This is the pointwise algebra behind the future integral summation-by-parts identity.

theorem HCPolySupport.euclideanForwardDifferenceQuotient_coordShift_neg_eq_backward {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanForwardDifferenceQuotient h i u (euclideanCoordShift (-h) i x) = euclideanBackwardDifferenceQuotient h i u x

A forward quotient at the backward-shifted point is the corresponding backward quotient.

theorem HCPolySupport.euclideanForwardDifferenceQuotient_eq_backwardDifferenceQuotient_neg {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) : euclideanForwardDifferenceQuotient h i u = euclideanBackwardDifferenceQuotient (-h) i u

A forward quotient with step h is the backward quotient with step -h.

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_sq_mul_forwardDifferenceQuotient {d : ℕ} (h : ℝ) (i : Fin d) (η u : Vec d → ℝ) (x : Vec d) : euclideanBackwardDifferenceQuotient h i (fun (y : Vec d) => η y ^ 2 * euclideanForwardDifferenceQuotient h i u y) x = h⁻¹ * (η x ^ 2 * euclideanForwardDifferenceQuotient h i u x - η (euclideanCoordShift (-h) i x) ^ 2 * euclideanBackwardDifferenceQuotient h i u x)

Backward quotient of the direct difference-quotient test η² D_i^+ u, expanded into its unshifted and shifted pieces.

theorem HCPolySupport.contDiff_comp_euclideanCoordShift {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (h : ℝ) (i : Fin d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => u (euclideanCoordShift h i x)

Smooth functions remain smooth after a coordinate shift.

theorem HCPolySupport.hasCompactSupport_comp_euclideanCoordShift {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) (h : ℝ) (i : Fin d) : HasCompactSupport fun (x : Vec d) => u (euclideanCoordShift h i x)

Compact support is preserved by precomposition with a coordinate shift.

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

Forward difference quotients of smooth functions are smooth.

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

Backward difference quotients of smooth functions are smooth.

theorem HCPolySupport.hasCompactSupport_euclideanForwardDifferenceQuotient {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) (h : ℝ) (i : Fin d) : HasCompactSupport (euclideanForwardDifferenceQuotient h i u)

Forward difference quotients of compactly supported functions are compactly supported.

theorem HCPolySupport.hasCompactSupport_euclideanBackwardDifferenceQuotient {d : ℕ} {u : Vec d → ℝ} (hu : HasCompactSupport u) (h : ℝ) (i : Fin d) : HasCompactSupport (euclideanBackwardDifferenceQuotient h i u)

Backward difference quotients of compactly supported functions are compactly supported.

theorem HCPolySupport.euclideanCoordDeriv_comp_euclideanCoordShift {d : ℕ} (h : ℝ) (i j : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanCoordDeriv j (fun (y : Vec d) => u (euclideanCoordShift h i y)) x = euclideanCoordDeriv j u (euclideanCoordShift h i x)

Coordinate derivatives commute with precomposition by a coordinate shift.

theorem HCPolySupport.euclideanCoordDeriv_sub {d : ℕ} {u v : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (i : Fin d) (x : Vec d) : euclideanCoordDeriv i (fun (y : Vec d) => u y - v y) x = euclideanCoordDeriv i u x - euclideanCoordDeriv i v x

Coordinate derivatives distribute over subtraction for smooth functions.

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

Coordinate derivatives commute with multiplication by a scalar on the right.

theorem HCPolySupport.euclideanCoordDeriv_euclideanForwardDifferenceQuotient {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (h : ℝ) (i j : Fin d) (x : Vec d) : euclideanCoordDeriv j (euclideanForwardDifferenceQuotient h i u) x = euclideanForwardDifferenceQuotient h i (euclideanCoordDeriv j u) x

Coordinate derivatives commute with forward coordinate difference quotients for smooth functions.

theorem HCPolySupport.euclideanCoordDeriv_euclideanBackwardDifferenceQuotient {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (h : ℝ) (i j : Fin d) (x : Vec d) : euclideanCoordDeriv j (euclideanBackwardDifferenceQuotient h i u) x = euclideanBackwardDifferenceQuotient h i (euclideanCoordDeriv j u) x

Coordinate derivatives commute with backward coordinate difference quotients for smooth functions.

theorem HCPolySupport.euclideanGradient_euclideanForwardDifferenceQuotient {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (h : ℝ) (i : Fin d) (x : Vec d) : euclideanGradient (euclideanForwardDifferenceQuotient h i u) x = fun (j : Fin d) => euclideanForwardDifferenceQuotient h i (euclideanCoordDeriv j u) x

Euclidean gradients commute with forward coordinate difference quotients for smooth functions.

theorem HCPolySupport.euclideanGradient_euclideanBackwardDifferenceQuotient {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (h : ℝ) (i : Fin d) (x : Vec d) : euclideanGradient (euclideanBackwardDifferenceQuotient h i u) x = fun (j : Fin d) => euclideanBackwardDifferenceQuotient h i (euclideanCoordDeriv j u) x

Euclidean gradients commute with backward coordinate difference quotients for smooth functions.

theorem HCPolySupport.euclideanGradient_comp_euclideanCoordShift {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) (x : Vec d) : euclideanGradient (fun (y : Vec d) => u (euclideanCoordShift h i y)) x = euclideanGradient u (euclideanCoordShift h i x)

Euclidean gradients commute with precomposition by a coordinate shift.

theorem HCPolySupport.euclideanBackwardDifferenceQuotient_eq_integral_coordDeriv_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {h : ℝ} (hh : h ≠ 0) (i : Fin d) (x : Vec d) : euclideanBackwardDifferenceQuotient h i u x = ∫ (t : ℝ) in 0..1, euclideanCoordDeriv i u (segmentBlend x t (euclideanCoordShift (-h) i x))

Pointwise FTC formula for a backward coordinate difference quotient of a smooth function.

theorem HCPolySupport.abs_euclideanBackwardDifferenceQuotient_le_integral_abs_coordDeriv_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {h : ℝ} (hh : h ≠ 0) (i : Fin d) (x : Vec d) : |euclideanBackwardDifferenceQuotient h i u x| ≤ ∫ (t : ℝ) in 0..1, |euclideanCoordDeriv i u (segmentBlend x t (euclideanCoordShift (-h) i x))|

Pointwise norm bound following from the FTC representation of a backward coordinate difference quotient.

theorem HCPolySupport.sq_intervalIntegral_abs_le_intervalIntegral_sq_abs_of_continuous {g : ℝ → ℝ} (hg : Continuous g) : (∫ (t : ℝ) in 0..1, |g t|) ^ 2 ≤ ∫ (t : ℝ) in 0..1, |g t| ^ 2

Jensen/Cauchy on the unit interval for a continuous real function.

theorem HCPolySupport.sq_euclideanBackwardDifferenceQuotient_le_integral_sq_coordDeriv_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {h : ℝ} (hh : h ≠ 0) (i : Fin d) (x : Vec d) : euclideanBackwardDifferenceQuotient h i u x ^ 2 ≤ ∫ (t : ℝ) in 0..1, euclideanCoordDeriv i u (segmentBlend x t (euclideanCoordShift (-h) i x)) ^ 2

Pointwise squared version of the smooth FTC/Jensen estimate for backward coordinate difference quotients.

theorem HCPolySupport.segmentBlend_euclideanCoordShift_neg_eq_euclideanCoordShift {d : ℕ} (h : ℝ) (i : Fin d) (x : Vec d) (t : ℝ) : segmentBlend x t (euclideanCoordShift (-h) i x) = euclideanCoordShift ((t - 1) * h) i x

The segment from x - h eᵢ to x is just a coordinate shift of x. This is the algebraic step behind collapsing the FTC/Jensen segment average by translation invariance.

theorem HCPolySupport.integral_comp_euclideanCoordShift_eq_integral {d : ℕ} (h : ℝ) (i : Fin d) (u : Vec d → ℝ) : ∫ (x : Vec d), u (euclideanCoordShift h i x) = ∫ (x : Vec d), u x

Whole-space translation invariance for a coordinate shift.

theorem HCPolySupport.integral_comp_segmentBlend_euclideanCoordShift_neg_eq_integral {d : ℕ} (h : ℝ) (i : Fin d) (t : ℝ) (u : Vec d → ℝ) : ∫ (x : Vec d), u (segmentBlend x t (euclideanCoordShift (-h) i x)) = ∫ (x : Vec d), u x

Combining the segment algebra with whole-space translation invariance: integrating along the segment from x - h eᵢ to x, for fixed t, has the same integral as the unshifted function.

theorem HCPolySupport.integral_sq_coordDeriv_comp_segmentBlend_euclideanCoordShift_neg_eq_integral {d : ℕ} (h : ℝ) (i : Fin d) (t : ℝ) (u : Vec d → ℝ) : ∫ (x : Vec d), euclideanCoordDeriv i u (segmentBlend x t (euclideanCoordShift (-h) i x)) ^ 2 = ∫ (x : Vec d), euclideanCoordDeriv i u x ^ 2

Fixed-time translation collapse for the squared coordinate derivative appearing in the smooth FTC/Jensen estimate.

theorem HCPolySupport.integrable_sq_coordDeriv_comp_segmentBlend_euclideanCoordShift_neg_prod {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hus : HasCompactSupport u) (h : ℝ) (i : Fin d) : MeasureTheory.Integrable (Function.uncurry fun (t : ℝ) (x : Vec d) => euclideanCoordDeriv i u (segmentBlend x t (euclideanCoordShift (-h) i x)) ^ 2) ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod MeasureTheory.volume)

Product integrability of the smooth segment-square integrand used to swap the t and x integrals in the quotient bound.

theorem HCPolySupport.segmentShift_derivativeSquare_integral_eq_integral {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hus : HasCompactSupport u) (h : ℝ) (i : Fin d) : ∫ (x : Vec d), ∫ (t : ℝ) in 0..1, euclideanCoordDeriv i u (segmentBlend x t (euclideanCoordShift (-h) i x)) ^ 2 = ∫ (x : Vec d), euclideanCoordDeriv i u x ^ 2

The integrated smooth FTC/Jensen segment term collapses to the unshifted coordinate-derivative square norm.

theorem HCPolySupport.integral_sq_euclideanBackwardDifferenceQuotient_le_integral_sq_coordDeriv {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hus : HasCompactSupport u) {h : ℝ} (hh : h ≠ 0) (i : Fin d) : ∫ (x : Vec d), euclideanBackwardDifferenceQuotient h i u x ^ 2 ≤ ∫ (x : Vec d), euclideanCoordDeriv i u x ^ 2

Smooth compact-support L² control of a backward coordinate difference quotient by the corresponding coordinate derivative.

theorem HCPolySupport.toReal_eLpNorm_two_sq_eq_integral_sq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) : (MeasureTheory.eLpNorm f 2 μ).toReal ^ 2 = ∫ (x : α), f x ^ 2 ∂μ

For real-valued L² functions, the square of the toReal eLpNorm is the integral of the pointwise square.

theorem HCPolySupport.eLpNorm_euclideanBackwardDifferenceQuotient_le_eLpNorm_coordDeriv {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hus : HasCompactSupport u) {h : ℝ} (hh : h ≠ 0) (i : Fin d) : MeasureTheory.eLpNorm (euclideanBackwardDifferenceQuotient h i u) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm (euclideanCoordDeriv i u) 2 MeasureTheory.volume

Smooth compact-support quotient control in eLpNorm form. This is the form used by the H¹₀ approximation bridge.

theorem HCPolySupport.integral_comp_euclideanCoordShift_mul_eq_integral_mul_comp_euclideanCoordShift_neg {d : ℕ} (h : ℝ) (i : Fin d) (u v : Vec d → ℝ) : ∫ (x : Vec d), u (euclideanCoordShift h i x) * v x = ∫ (x : Vec d), u x * v (euclideanCoordShift (-h) i x)

Whole-space translation change of variables for a coordinate shift. This is the measure-theoretic core of finite-difference summation by parts.

theorem HCPolySupport.integral_vecDot_comp_euclideanCoordShift_eq_integral_vecDot_comp_euclideanCoordShift_neg {d : ℕ} (h : ℝ) (i : Fin d) (F G : Vec d → Vec d) : ∫ (x : Vec d), vecDot (F (euclideanCoordShift h i x)) (G x) = ∫ (x : Vec d), vecDot (F x) (G (euclideanCoordShift (-h) i x))

Vector-valued whole-space translation change of variables for coordinate shifts, paired by vecDot.

theorem HCPolySupport.integral_forwardDifference_mul_eq_neg_integral_mul_backwardDifference {d : ℕ} {u v : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hus : HasCompactSupport u) (h : ℝ) (i : Fin d) : ∫ (x : Vec d), euclideanForwardDifferenceQuotient h i u x * v x = -∫ (x : Vec d), u x * euclideanBackwardDifferenceQuotient h i v x

Whole-space finite-difference summation by parts. The compact-support assumption on u supplies the integrability needed to expand the two difference quotients into ordinary Lebesgue integrals.