Morrey's inequality on a one-dimensional ball

The d = 1 warm-up for the Morrey embedding: a function with an L² weak derivative on an interval has a 1/2-Hölder representative. The singular kernel of the general-dimension argument degenerates to the constant 1 here, so the whole content is the one-dimensional weak fundamental theorem of calculus (recovering u a.e. from its weak derivative) followed by Cauchy-Schwarz.

def EllipticPdes.Embedding.coordEquiv : EuclideanSpace ℝ (Fin 1) ≃ᵐ ℝ

The measurable equivalence identifying EuclideanSpace ℝ (Fin 1) with ℝ via the single coordinate.

Equations

• EllipticPdes.Embedding.coordEquiv = (MeasurableEquiv.toLp 2 (Fin 1 → ℝ)).symm.trans (MeasurableEquiv.funUnique (Fin 1) ℝ)

@[simp]

theorem EllipticPdes.Embedding.coordEquiv_apply (x : EuclideanSpace ℝ (Fin 1)) : coordEquiv x = x.ofLp 0

coordEquiv sends a point to its single coordinate.

theorem EllipticPdes.Embedding.coordEquiv_symm_coord (t : ℝ) : (coordEquiv.symm t).ofLp 0 = t

The single coordinate of coordEquiv.symm t is t.

@[simp]

theorem EllipticPdes.Embedding.coordEquiv_symm_eq (t : ℝ) : coordEquiv.symm t = !₂[t]

coordEquiv.symm t is the one-dimensional Euclidean point !₂[t].

theorem EllipticPdes.Embedding.coordEquiv_measurePreserving : MeasureTheory.MeasurePreserving (⇑coordEquiv) MeasureTheory.volume MeasureTheory.volume

coordEquiv is volume preserving between the Euclidean line and ℝ.

theorem EllipticPdes.Embedding.dist_eq_coord (x y : EuclideanSpace ℝ (Fin 1)) : dist x y = |x.ofLp 0 - y.ofLp 0|

EuclideanSpace ℝ (Fin 1) distance collapses to the distance of the single coordinate.

theorem EllipticPdes.Embedding.coordEquiv_symm_preimage_ball (c : EuclideanSpace ℝ (Fin 1)) (r : ℝ) : ⇑coordEquiv.symm ⁻¹' Metric.ball c r = Set.Ioo (c.ofLp 0 - r) (c.ofLp 0 + r)

The ball Metric.ball c r corresponds, under coordEquiv, to the coordinate interval Ioo (c 0 - r) (c 0 + r).

theorem EllipticPdes.Embedding.ball_setIntegral_eq_intervalIntegral {c : EuclideanSpace ℝ (Fin 1)} {r : ℝ} (hr : 0 < r) (F : EuclideanSpace ℝ (Fin 1) → ℝ) : ∫ (x : EuclideanSpace ℝ (Fin 1)) in Metric.ball c r, F x = ∫ (t : ℝ) in c.ofLp 0 - r..c.ofLp 0 + r, F !₂[t]

Transport a set integral over a 1-D ball into an interval integral over the corresponding coordinate interval.

theorem EllipticPdes.Embedding.coordEquiv_preimage_Ioo (c : EuclideanSpace ℝ (Fin 1)) (r : ℝ) : ⇑coordEquiv ⁻¹' Set.Ioo (c.ofLp 0 - r) (c.ofLp 0 + r) = Metric.ball c r

The ball corresponds, under coordEquiv, to the coordinate interval, in the forward direction.

theorem EllipticPdes.Embedding.partialD_coord_comp {ψ : ℝ → ℝ} (hψ : Differentiable ℝ ψ) (x : EuclideanSpace ℝ (Fin 1)) : Sobolev.partialD 0 (fun (y : EuclideanSpace ℝ (Fin 1)) => ψ (y.ofLp 0)) x = deriv ψ (x.ofLp 0)

The classical partial derivative of a lifted 1-D test function is the classical derivative of the interval function, at the corresponding coordinate.

theorem EllipticPdes.Embedding.proj_eq_coordEquiv : ⇑(EuclideanSpace.proj 0) = ⇑coordEquiv

The coordinate projection agrees with coordEquiv as a bare function.

theorem EllipticPdes.Embedding.contDiff_lift {φ : ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin 1)) => φ (x.ofLp 0)

Lifting a smooth interval test function compactly supported in Ioo a b to EuclideanSpace ℝ (Fin 1) is a smooth test function compactly supported in the ball.

theorem EllipticPdes.Embedding.support_lift (φ : ℝ → ℝ) : (Function.support fun (x : EuclideanSpace ℝ (Fin 1)) => φ (x.ofLp 0)) = ⇑coordEquiv ⁻¹' Function.support φ

The support of a lifted test function is the coordinate preimage of the original support.

theorem EllipticPdes.Embedding.tsupport_lift_subset (φ : ℝ → ℝ) : (tsupport fun (x : EuclideanSpace ℝ (Fin 1)) => φ (x.ofLp 0)) ⊆ ⇑coordEquiv ⁻¹' tsupport φ

The topological support of a lifted test function is contained in the coordinate preimage of the original topological support.

theorem EllipticPdes.Embedding.hasCompactSupport_and_tsupport_lift {φ : ℝ → ℝ} {c : EuclideanSpace ℝ (Fin 1)} {r : ℝ} (hsub : tsupport φ ⊆ Set.Ioo (c.ofLp 0 - r) (c.ofLp 0 + r)) : (HasCompactSupport fun (x : EuclideanSpace ℝ (Fin 1)) => φ (x.ofLp 0)) ∧ (tsupport fun (x : EuclideanSpace ℝ (Fin 1)) => φ (x.ofLp 0)) ⊆ Metric.ball c r

A lifted test function whose original is compactly supported in (a, b) has compact support contained in the ball Metric.ball c r.

theorem EllipticPdes.Embedding.morrey_ball_oneDim (c : EuclideanSpace ℝ (Fin 1)) {r : ℝ} (hr : 0 < r) : ∃ (C : NNReal), ∀ (u g : EuclideanSpace ℝ (Fin 1) → ℝ), MeasureTheory.IntegrableOn u (Metric.ball c r) MeasureTheory.volume → MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Metric.ball c r)) → (HasWeakGradOn (Metric.ball c r) u fun (x : Fin 1) => g) → ∃ (u' : EuclideanSpace ℝ (Fin 1) → ℝ), u' =ᵐ[MeasureTheory.volume.restrict (Metric.ball c r)] u ∧ HolderOnWith (C * (MeasureTheory.eLpNorm g 2 (MeasureTheory.volume.restrict (Metric.ball c r))).toNNReal) (morreyExponent 1 2) u' (Metric.ball c r)

Morrey on an interval. A function with an L² weak derivative on a 1-D ball has a C^{0,1/2} representative, with Hölder constant linear in the L² norm of its derivative.

Terminal result of the library, the one-dimensional endpoint of the Morrey chain. Nothing else consumes it.