Finite-energy estimate for the radial homotopy operator

In three dimensions, the operator u ↦ ∫₀¹ t • u(t • x) dt has L² operator norm at most two. The substitution t = r² reduces the estimate to ordinary Cauchy--Schwarz and exactly cancels the Jacobian of dilation. Only continuity and finite energy are needed; no derivative integrability is assumed.

theorem Euler.ComparatorBridge.radial_average_eq_quadratic (u : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hu : Continuous u) (x : EuclideanSpace ℝ (Fin 3)) : ∫ (t : ℝ) in 0..1, t • u (t • x) = ∫ (r : ℝ) in 0..1, (2 * r ^ 3) • u (r ^ 2 • x)

A square substitution removes the singular weight in the radial estimate.

theorem Euler.ComparatorBridge.quadratic_dilation_energy (u : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) {r : ℝ} (hr : r ≠ 0) : ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖(2 * r ^ 3) • u (r ^ 2 • x)‖ ^ 2 = 4 * ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖u x‖ ^ 2

Squared L² energy of a dilated field, with its compensating factor.

theorem Euler.ComparatorBridge.quadratic_radial_action (u : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hu : Continuous u) (hL2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin 3)) => ∫ (r : ℝ) in Set.Ioc 0 1, ‖(2 * r ^ 3) • u (r ^ 2 • x)‖ ^ 2) MeasureTheory.volume ∧ ∫ (x : EuclideanSpace ℝ (Fin 3)), ∫ (r : ℝ) in Set.Ioc 0 1, ‖(2 * r ^ 3) • u (r ^ 2 • x)‖ ^ 2 = 4 * ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖u x‖ ^ 2

The quadratic parametrization has finite total action, exactly four times that of the original field.

theorem Euler.ComparatorBridge.radial_average_sq_le_action (u : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hu : Continuous u) (x : EuclideanSpace ℝ (Fin 3)) : ‖∫ (t : ℝ) in 0..1, t • u (t • x)‖ ^ 2 ≤ ∫ (r : ℝ) in Set.Ioc 0 1, ‖(2 * r ^ 3) • u (r ^ 2 • x)‖ ^ 2

Pointwise Cauchy--Schwarz for the regularized radial parametrization.

theorem Euler.ComparatorBridge.radial_average_memLp_and_energy (u : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hu : Continuous u) (hL2 : MeasureTheory.MemLp u 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin 3)) => ∫ (t : ℝ) in 0..1, t • u (t • x)) 2 MeasureTheory.volume ∧ ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖∫ (t : ℝ) in 0..1, t • u (t • x)‖ ^ 2 ≤ 4 * ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖u x‖ ^ 2

The radial homotopy average preserves L², with operator norm at most two.