Ray fundamental theorem of calculus

For a smooth function φ, the increment φ (x + v) - φ x equals the integral, over [0, 1], of the directional derivative (fderiv ℝ φ (x + t • v)) v along the segment t ↦ x + t • v. This is the pointwise identity consumed by the potential-estimate step of the Morrey embedding.

theorem EllipticPdes.Embedding.sub_eq_intervalIntegral_fderiv {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x v : EuclideanSpace ℝ (Fin d)) : φ (x + v) - φ x = ∫ (t : ℝ) in 0..1, (fderiv ℝ φ (x + t • v)) v

Ray fundamental theorem of calculus. For smooth φ, the increment along the segment from x to x + v is the integral of the directional derivative.

theorem EllipticPdes.Embedding.oscillation_eq_average_ray_set {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (x : EuclideanSpace ℝ (Fin d)) {W : Set (EuclideanSpace ℝ (Fin d))} (hWmeas : MeasurableSet W) (hpos : MeasureTheory.volume W ≠ 0) (htop : MeasureTheory.volume W ≠ ⊤) (hint : MeasureTheory.IntegrableOn φ W MeasureTheory.volume) : (⨍ (y : EuclideanSpace ℝ (Fin d)) in W, φ y) - φ x = ⨍ (y : EuclideanSpace ℝ (Fin d)) in W, ∫ (t : ℝ) in 0..1, (fderiv ℝ φ (x + t • (y - x))) (y - x)

Ray-FTC average identity over a measurable set. For smooth φ and a measurable set W of positive finite measure on which φ is integrable, the oscillation of the W-average of φ about the value φ x equals the average over W of the ray integral of the directional derivative from x towards the running point y. This is the mechanical half of the potential estimate over a general averaging domain.

theorem EllipticPdes.Embedding.oscillation_eq_average_ray {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (c x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : (⨍ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball c r, φ y) - φ x = ⨍ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball c r, ∫ (t : ℝ) in 0..1, (fderiv ℝ φ (x + t • (y - x))) (y - x)

Ray-FTC average identity (Morrey rung 4a). The ball specialisation of oscillation_eq_average_ray_set: for smooth φ, the oscillation of the ball-average of φ about φ x equals the average over the ball of the gradient line integral from x.

theorem EllipticPdes.Embedding.kernel_bound_convex {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hd : 0 < d) (x : EuclideanSpace ℝ (Fin d)) {D : ℝ} (hD : 0 < D) {W : Set (EuclideanSpace ℝ (Fin d))} (hWmeas : MeasurableSet W) (hWconv : Convex ℝ W) (hxW : x ∈ W) (hWsub : W ⊆ Metric.ball x D) : ∫⁻ (y : EuclideanSpace ℝ (Fin d)) in W, ∫⁻ (t : ℝ) in Set.Ioc 0 1, ‖fderiv ℝ φ (x + t • (y - x))‖ₑ * ‖y - x‖ₑ ≤ ENNReal.ofReal (D ^ d / ↑d) * ∫⁻ (z : EuclideanSpace ℝ (Fin d)) in W, ‖fderiv ℝ φ z‖ₑ / ‖z - x‖ₑ ^ (d - 1)

Morrey kernel bound (convex form). The double gradient line integral over a bounded convex measurable set W containing the base point x is controlled by the Riesz potential of the gradient, with a dimensional factor D^d/d, where D is any radius with W ⊆ ball x D. Proof: Tonelli swap, the affine change of variables potential_inner_cov for each scale t, the region containment W_t ⊆ W ∩ ball x (D t) (using convexity of W), a second Tonelli swap, and the per-point Riesz factor inner_t_bound. Specialising W = ball c r, D = 2 r recovers the centred estimate.

theorem EllipticPdes.Embedding.riesz_potential_integrableOn {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hd : 0 < d) (c x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (_hr : 0 < r) (hx : x ∈ Metric.ball c r) : MeasureTheory.IntegrableOn (fun (z : EuclideanSpace ℝ (Fin d)) => ‖fderiv ℝ φ z‖ / dist x z ^ (d - 1)) (Metric.ball c r) MeasureTheory.volume

Integrability of the Riesz potential. For smooth φ and x in the ball, the singular integrand ‖∇φ‖ / dist x ·^{d-1} is integrable on the ball: the singularity dist x ·^{-(d-1)} has exponent d - 1 < d, and ‖∇φ‖ is bounded on the compact closure. This is what makes the right-hand side of the potential estimate finite (hence the estimate meaningful).

theorem EllipticPdes.Embedding.exists_potential_bound {d : ℕ} (hd : 0 < d) : ∃ (Cd : NNReal), ∀ (φ : EuclideanSpace ℝ (Fin d) → ℝ), ContDiff ℝ (↑⊤) φ → ∀ (c : EuclideanSpace ℝ (Fin d)) {r : ℝ}, 0 < r → ∀ x ∈ Metric.ball c r, |φ x - ⨍ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball c r, φ y| ≤ ↑Cd * ∫ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball c r, ‖fderiv ℝ φ y‖ / dist x y ^ (d - 1)

Morrey potential estimate for smooth functions. For a smooth φ and any point x of a ball, the oscillation of φ about its ball average is controlled by the Riesz potential of the gradient, with a dimensional constant Cd = 2^d / (d ω_d). This is the analytic heart of the Morrey embedding, assembled from the ray-FTC average identity, the kernel bound, and the integrability of the Riesz potential.

theorem EllipticPdes.Embedding.oscillation_le_potential_convex {d : ℕ} [Nontrivial (EuclideanSpace ℝ (Fin d))] {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hd : 0 < d) (a : EuclideanSpace ℝ (Fin d)) {W : Set (EuclideanSpace ℝ (Fin d))} (hWmeas : MeasurableSet W) (hWconv : Convex ℝ W) (haW : a ∈ W) (hWpos : MeasureTheory.volume W ≠ 0) (hWtop : MeasureTheory.volume W ≠ ⊤) {R : ℝ} (hR : 0 < R) (hWsub : W ⊆ Metric.ball a R) (hint : MeasureTheory.IntegrableOn (fun (z : EuclideanSpace ℝ (Fin d)) => ‖fderiv ℝ φ z‖ / dist a z ^ (d - 1)) W MeasureTheory.volume) : |φ a - ⨍ (y : EuclideanSpace ℝ (Fin d)) in W, φ y| ≤ R ^ d / (↑d * MeasureTheory.volume.real W) * ∫ (z : EuclideanSpace ℝ (Fin d)) in W, ‖fderiv ℝ φ z‖ / dist a z ^ (d - 1)

Potential estimate over a convex averaging domain. For smooth φ, a bounded convex measurable set W of positive finite measure containing the base point a, with W ⊆ ball a R, the oscillation of φ about its W-average is controlled by the Riesz potential of the gradient over W, with the explicit factor R^d/(d · |W|). This is the convex-lens analogue of exists_potential_bound; combined with the subset Riesz-kernel bound it yields the two-point Hölder estimate.