A parabolic Vitali covering estimate

This file records the measure estimate obtained by applying the Vitali covering theorem to the metric balls associated with the parabolic cylinders.

@[reducible, inline]

abbrev CKN.Foundation.Parabolic.coveringParabolicMetricBall (c : ParabolicPoint) (r : ℝ) : Set ParabolicPoint

Explicit parabolic metric-ball family used in the covering argument.

Equations

• CKN.Foundation.Parabolic.coveringParabolicMetricBall c r = Metric.ball c r

theorem CKN.Foundation.Parabolic.measurableSet_parabolicCylinder (x : Vec3) (t r : ℝ) : MeasurableSet (parabolicCylinder x t r)

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

theorem CKN.Foundation.Parabolic.parabolicHausdorffMeasure_one_le_integral_of_small_cylinders {g : ParabolicPoint → ENNReal} {U S : Set ParabolicPoint} : Measurable g → IsOpen U → S ⊆ U → ∀ {ε : NNReal} (hε : 0 < ε) (hsmall : ∀ z ∈ S, ∀ (n : ℕ), ∃ (r : ℝ), 0 < r ∧ r < 1 / ↑(n + 1) ∧ parabolicCylinder z.1 z.2 r ⊆ U ∧ ↑ε * ENNReal.ofReal r < ∫⁻ (y : ParabolicPoint) in parabolicCylinder z.1 z.2 r, g y), ∫⁻ (y : ParabolicPoint) in U, g y < ⊤ → (parabolicHausdorffMeasure 1) S ≤ 10 / ↑ε * ∫⁻ (y : ParabolicPoint) in U, g y

noncomputable def CKN.Foundation.Parabolic.parabolicVolumeConstant : ENNReal

Volume coefficient for the parabolic covering estimates.

Equations

• CKN.Foundation.Parabolic.parabolicVolumeConstant = ENNReal.ofReal (4 ^ 5) * MeasureTheory.volume (CKN.Foundation.Parabolic.parabolicCylinder 0 0 1)

theorem CKN.Foundation.Parabolic.parabolicHausdorffMeasure_one_lt_top_imp_volume_zero {E : Set ParabolicPoint} (hE : (parabolicHausdorffMeasure 1) E < ⊤) : MeasureTheory.volume E = 0

theorem CKN.Foundation.Parabolic.parabolicHausdorffMeasure_one_eq_zero_of_small_cylinders {g : ParabolicPoint → ENNReal} (hg : Measurable g) {U S : Set ParabolicPoint} (hU : IsOpen U) (hSU : S ⊆ U) {ε : NNReal} (hε : 0 < ε) (hsmall : ∀ z ∈ S, ∀ (n : ℕ), ∃ (r : ℝ), 0 < r ∧ r < 1 / ↑(n + 1) ∧ parabolicCylinder z.1 z.2 r ⊆ U ∧ ↑ε * ENNReal.ofReal r < ∫⁻ (y : ParabolicPoint) in parabolicCylinder z.1 z.2 r, g y) (hfin : ∫⁻ (y : ParabolicPoint), g y < ⊤) : (parabolicHausdorffMeasure 1) S = 0