Hölder bounds for the parabolic metric

This module names the seminorm used by the space-time regularity statements. The measure-theoretic representative predicate records agreement on a set.

def CKN.Foundation.Parabolic.ParabolicHolderSeminormLE (U : Set ParabolicPoint) (g : ParabolicPoint → ℝ) (α K : ℝ) : Prop

Pointwise Hölder seminorm bound with respect to parabolic distance.

Equations

• CKN.Foundation.Parabolic.ParabolicHolderSeminormLE U g α K = ∀ x ∈ U, ∀ y ∈ U, |g x - g y| ≤ K * CKN.Foundation.Parabolic.parabolicDist x y ^ α

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

Existence of an a.e.-equal representative satisfying a parabolic Hölder bound.

Equations

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

theorem CKN.Foundation.Parabolic.parabolicDist_nonneg (x y : ParabolicPoint) : 0 ≤ parabolicDist x y

theorem CKN.Foundation.Parabolic.ParabolicHolderSeminormLE.mono_set {U V : Set ParabolicPoint} {g : ParabolicPoint → ℝ} {α K : ℝ} (h : ParabolicHolderSeminormLE U g α K) (hVU : V ⊆ U) : ParabolicHolderSeminormLE V g α K

theorem CKN.Foundation.Parabolic.ParabolicHolderSeminormLE.hasRepresentative {U : Set ParabolicPoint} {f : ParabolicPoint → ℝ} {α K : ℝ} (h : ParabolicHolderSeminormLE U f α K) : HasParabolicHolderRepresentativeOn U f α K