Regularized Hardy inequality

The regularized inverse-square weight is a valid Schwartz multiplier.

Each component of the regularized Hardy field has temperate growth.

theorem LiebThirring.hasTemperateGrowth_hardy_weight {ε : ℝ} (hε : 0 < ε) (c : Position) : Function.HasTemperateGrowth fun (x : Position) => (‖x - c‖ ^ 2 + ε ^ 2)⁻¹

The regularized inverse-square weight is a valid Schwartz multiplier.

theorem LiebThirring.hasTemperateGrowth_hardy_component {ε : ℝ} (hε : 0 < ε) (c v : Position) : Function.HasTemperateGrowth fun (x : Position) => inner ℝ (x - c) v / (‖x - c‖ ^ 2 + ε ^ 2)

Each component of the regularized Hardy field has temperate growth.

theorem LiebThirring.fderiv_hardy_component {ε : ℝ} (hε : 0 < ε) (c x v w : Position) : (fderiv ℝ (fun (y : Position) => inner ℝ (y - c) v / (‖y - c‖ ^ 2 + ε ^ 2)) x) w = inner ℝ w v / (‖x - c‖ ^ 2 + ε ^ 2) - 2 * inner ℝ (x - c) v * inner ℝ (x - c) w / (‖x - c‖ ^ 2 + ε ^ 2) ^ 2

Directional derivative of the regularized Hardy field component.

theorem LiebThirring.sum_fderiv_hardy_component {ε : ℝ} (hε : 0 < ε) (c x : Position) : ∑ i : Fin 3, (fderiv ℝ (fun (y : Position) => inner ℝ (y - c) ((EuclideanSpace.basisFun (Fin 3) ℝ) i) / (‖y - c‖ ^ 2 + ε ^ 2)) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) i) = (‖x - c‖ ^ 2 + 3 * ε ^ 2) / (‖x - c‖ ^ 2 + ε ^ 2) ^ 2

The coordinate trace of the regularized Hardy field in dimension three.

theorem LiebThirring.hasTemperateGrowth_fderiv_hardy_component {ε : ℝ} (hε : 0 < ε) (c v w : Position) : Function.HasTemperateGrowth fun (x : Position) => (fderiv ℝ (fun (y : Position) => inner ℝ (y - c) v / (‖y - c‖ ^ 2 + ε ^ 2)) x) w

The field derivative is also a valid Schwartz multiplier.

theorem LiebThirring.integrable_temperate_mul_schwartz {a : Position → ℝ} (ha : Function.HasTemperateGrowth a) (g : SchwartzMap Position ℝ) : MeasureTheory.Integrable (fun (x : Position) => a x * g x) MeasureTheory.volume

A temperate multiplier times a scalar Schwartz test is integrable.

theorem LiebThirring.integral_hardy_component_mul_fderiv {ε : ℝ} (hε : 0 < ε) (c v : Position) (g : SchwartzMap Position ℝ) : ∫ (x : Position), inner ℝ (x - c) v / (‖x - c‖ ^ 2 + ε ^ 2) * (fderiv ℝ (⇑g) x) v = -∫ (x : Position), (fderiv ℝ (fun (y : Position) => inner ℝ (y - c) v / (‖y - c‖ ^ 2 + ε ^ 2)) x) v * g x

Integration by parts against one component of the regularized field.

theorem LiebThirring.fderiv_schwartz_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : SchwartzMap Position E) (x v : Position) : (fderiv ℝ (fun (y : Position) => ‖f y‖ ^ 2) x) v = 2 * inner ℝ (f x) ((fderiv ℝ (⇑f) x) v)

The derivative of the squared Hilbert norm, evaluated in one direction.

theorem LiebThirring.integral_hardy_component_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ε : ℝ} (hε : 0 < ε) (c v : Position) (f : SchwartzMap Position E) : ∫ (x : Position), (fderiv ℝ (fun (y : Position) => inner ℝ (y - c) v / (‖y - c‖ ^ 2 + ε ^ 2)) x) v * ‖f x‖ ^ 2 = -2 * ∫ (x : Position), inner ℝ (x - c) v / (‖x - c‖ ^ 2 + ε ^ 2) * inner ℝ (f x) ((fderiv ℝ (⇑f) x) v)

Integration by parts against the squared norm of a Hilbert-valued Schwartz map.

theorem LiebThirring.hardy_component_young {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : ℝ) (u v : E) : -2 * a * inner ℝ u v ≤ a ^ 2 * ‖u‖ ^ 2 / 2 + 2 * ‖v‖ ^ 2

The pointwise square estimate used to absorb half the weighted mass.

theorem LiebThirring.integrable_temperate_mul_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : Position → ℝ} (ha : Function.HasTemperateGrowth a) (f : SchwartzMap Position E) : MeasureTheory.Integrable (fun (x : Position) => a x * ‖f x‖ ^ 2) MeasureTheory.volume

A temperate multiplier times the squared Schwartz norm is integrable.

theorem LiebThirring.integral_hardy_regularized_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ε : ℝ} (hε : 0 < ε) (c : Position) (f : SchwartzMap Position E) : ∫ (x : Position), (‖x - c‖ ^ 2 + ε ^ 2)⁻¹ * ‖f x‖ ^ 2 ≤ 4 * ∑ i : Fin 3, ∫ (x : Position), ‖(fderiv ℝ (⇑f) x) ((EuclideanSpace.basisFun (Fin 3) ℝ) i)‖ ^ 2

The regularized Hardy estimate with constant four, uniform in the pole and scale.