Campanato oscillations on parabolic cylinders

The L^p oscillation of a function on a parabolic cylinder, the Campanato bound it satisfies on a region, the tail constant of the dyadic geometric series, and the comparison of the average of |f| on a subset with the average on the ambient set. The oscillations use genuine space-time averages.

instance CKN.Foundation.Parabolic.campanatoParabolicVolumeIsLocallyFinite : MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume

noncomputable def CKN.Foundation.Parabolic.ParabolicCylinderLpOscillation (f : ParabolicPoint → ℝ) (x : Vec3) (t r p : ℝ) : ℝ

Normalized Lᵖ oscillation about the mean on a backward parabolic cylinder.

Equations

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

def CKN.Foundation.Parabolic.ParabolicCylinderCampanatoBoundOn (f : ParabolicPoint → ℝ) (U : Set ParabolicPoint) (R α K p : ℝ) : Prop

Uniform power-decay bound for cylinder oscillations up to a prescribed radius.

Equations

• CKN.Foundation.Parabolic.ParabolicCylinderCampanatoBoundOn f U R α K p = ∀ z ∈ U, ∀ {r : ℝ}, 0 < r → r ≤ R → CKN.Foundation.Parabolic.ParabolicCylinderLpOscillation f z.1 z.2 r p ≤ K * r ^ α

noncomputable def CKN.Foundation.Parabolic.parabolicCampanatoTailConstant (α : ℝ) : ℝ

Geometric-series coefficient for summing dyadic Campanato oscillations.

Equations

• CKN.Foundation.Parabolic.parabolicCampanatoTailConstant α = 1 / (1 - 2 ^ (-α))

theorem CKN.Foundation.Parabolic.average_abs_le_outer_average_abs {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {A B : Set α} (hBA : B ⊆ A) (hApos : 0 < μ A) (hAtop : μ A < ⊤) (hBpos : 0 < μ B) (hBtop : μ B < ⊤) (hfA : MeasureTheory.IntegrableOn f A μ) : ⨍ (x : α) in B, |f x| ∂μ ≤ (μ A).toReal / (μ B).toReal * ⨍ (x : α) in A, |f x| ∂μ