Global Hölder functions in Lᵖ

This file proves that a globally Hölder function with finite Lᵖ norm is bounded and bundles it as an element of the global Hölder Banach space. The pointwise estimate compares the function with its average on a unit ball: Hölder continuity controls the difference from the average, while Hölder's inequality controls the average itself.

Main declarations

• HolderWith.enorm_le_add_eLpNorm: a global Hölder function in Lᵖ has a pointwise bound.
• HolderWith.toHolderSpace: bundle a global Hölder Lᵖ function in TauCeti.HolderSpace.
• HolderWith.norm_toHolderSpace_le: the resulting Hölder-space norm estimate.

theorem HolderWith.enorm_le_add_eLpNorm {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {g : E → F} {C α : NNReal} {p : ENNReal} (hg : HolderWith C α g) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hgLp : MeasureTheory.MemLp g p mu) (x : E) : ‖g x‖ₑ ≤ ↑C + mu (Metric.ball 0 1) ^ (-p.toReal⁻¹) * MeasureTheory.eLpNorm g p mu

A globally Hölder function with finite Lᵖ norm is pointwise bounded. At unit scale the bound is the sum of its Hölder constant and the Lᵖ norm multiplied by the inverse p-th power of the volume of the unit ball.

noncomputable def HolderWith.toHolderSpace {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {g : E → F} {C α : NNReal} {p : ENNReal} (hg : HolderWith C α g) (hα : 0 < α) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hgLp : MeasureTheory.MemLp g p mu) : TauCeti.HolderSpace α E F

A global Hölder function in Lᵖ, bundled as an element of the Hölder Banach space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HolderWith.toHolderSpace_apply {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {g : E → F} {C α : NNReal} {p : ENNReal} (hg : HolderWith C α g) (hα : 0 < α) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hgLp : MeasureTheory.MemLp g p mu) (x : E) : ↑(hg.toHolderSpace hα hp hp' hgLp).toHolderSubmodule x = g x

The Hölder-space bundling does not change the underlying function.

theorem HolderWith.norm_toHolderSpace_le {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {g : E → F} {C α : NNReal} {p : ENNReal} (hg : HolderWith C α g) (hα : 0 < α) (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hgLp : MeasureTheory.MemLp g p mu) : ‖hg.toHolderSpace hα hp hp' hgLp‖ ≤ (↑C + mu (Metric.ball 0 1) ^ (-p.toReal⁻¹) * MeasureTheory.eLpNorm g p mu).toReal + ↑C

The Hölder-space norm is controlled by the pointwise bound and the given Hölder constant.