Difference quotients on L²(ℝⁿ)

The difference quotient Dₖʰ u(x) = (u(x + h eₖ) - u(x)) / h drives the interior regularity theory (Evans, Partial Differential Equations (2nd ed.), §5.8.2 and §6.3.1). It is realised here as a continuous linear map on the whole-space space EucL2 d, built from the translation isometry transL2, so that its adjoint and norm bounds descend from translation invariance of Lebesgue measure.

noncomputable def EllipticPdes.Regularity.hshift {d : ℕ} (k : Fin d) (h : ℝ) : EuclideanSpace ℝ (Fin d)

The shift vector h • eₖ in the k-th coordinate direction.

Equations

• EllipticPdes.Regularity.hshift k h = h • EuclideanSpace.single k 1

noncomputable def EllipticPdes.Regularity.diffQuot {d : ℕ} (k : Fin d) (h : ℝ) : ↥(MeasureTheory.EucL2 d) →L[ℝ] ↥(MeasureTheory.EucL2 d)

The forward difference quotient Dₖʰ u = (τ_{h eₖ} u - u) / h as a continuous linear map on L²(ℝⁿ). For h = 0 it is the zero map.

Equations

• EllipticPdes.Regularity.diffQuot k h = h⁻¹ • ((MeasureTheory.transL2 (EllipticPdes.Regularity.hshift k h)).toContinuousLinearMap - ContinuousLinearMap.id ℝ ↥(MeasureTheory.EucL2 d))

@[simp]

theorem EllipticPdes.Regularity.diffQuot_zero {d : ℕ} (k : Fin d) : diffQuot k 0 = 0

The difference quotient vanishes identically at h = 0.

theorem EllipticPdes.Regularity.coeFn_diffQuot {d : ℕ} (k : Fin d) (h : ℝ) (u : ↥(MeasureTheory.EucL2 d)) : ↑↑((diffQuot k h) u) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ (Fin d)) => (↑↑u (x + hshift k h) - ↑↑u x) / h

The pointwise a.e. formula for the difference quotient: Dₖʰ u(x) = (u(x + h eₖ) - u(x)) / h.

theorem EllipticPdes.Regularity.transL2_inner_adjoint {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (u w : ↥(MeasureTheory.EucL2 d)) : inner ℝ ((MeasureTheory.transL2 v) u) w = inner ℝ u ((MeasureTheory.transL2 (-v)) w)

Translation by v is adjoint to translation by -v in the real L² inner product: ⟪τ_v u, w⟫ = ⟪u, τ_{-v} w⟫. This is the continuous shadow of discrete summation by parts, and rests on translation invariance of Lebesgue measure (Evans, Partial Differential Equations (2nd ed.), §5.8.2).

theorem EllipticPdes.Regularity.hshift_neg {d : ℕ} (k : Fin d) (h : ℝ) : hshift k (-h) = -hshift k h

The shift vector negates under negation of the step: h eₖ ↦ -(h eₖ) as h ↦ -h.

theorem EllipticPdes.Regularity.diffQuot_inner_adjoint {d : ℕ} (k : Fin d) (h : ℝ) (u w : ↥(MeasureTheory.EucL2 d)) : inner ℝ ((diffQuot k h) u) w = -inner ℝ u ((diffQuot k (-h)) w)

Discrete integration by parts. The difference quotient Dₖʰ is adjoint, up to a sign, to the backward difference quotient Dₖ⁻ʰ: ⟪Dₖʰ u, w⟫ = -⟪u, Dₖ⁻ʰ w⟫. This is the discretised analogue of integration by parts underlying the Caccioppoli-type interior estimate (Evans, Partial Differential Equations (2nd ed.), §5.8.2, proof of Theorem 3).