Documentation

LeanPool.CaffarelliKohnNirenberg.Foundation.Parabolic.Doubling

Doubling geometry for parabolic volume #

The parabolic metric has homogeneous dimension five. The lemmas below record the corresponding scaling of the spatial balls and parabolic cylinders, then use the cylinder/metric-ball comparison from Basic to provide the doubling instance required by metric covering arguments.

source
def CKN.Foundation.Parabolic.doublingVec3ScaleLinear (a : ℝ) :
Vec3 →ₗ[ℝ] Vec3

Linear spatial dilation used in the parabolic doubling calculation.

Equations
Instances For
    source
    theorem CKN.Foundation.Parabolic.volume_vec3Ball_scale {a r : ℝ} (ha : 0 < a) :
    MeasureTheory.volume (vec3Ball 0 (a * r)) = ENNReal.ofReal (a ^ 3) * MeasureTheory.volume (vec3Ball 0 r)
    source
    theorem CKN.Foundation.Parabolic.volume_parabolicCylinder_radius_scale {x : Vec3} {t r a : ℝ} (ha : 0 < a) :
    MeasureTheory.volume (parabolicCylinder x t (a * r)) = ENNReal.ofReal (a ^ 5) * MeasureTheory.volume (parabolicCylinder x t r)
    source
    theorem CKN.Foundation.Parabolic.volume_parabolicCylinder_time (x : Vec3) (t₁ t₂ r : ℝ) :
    MeasureTheory.volume (parabolicCylinder x t₁ r) = MeasureTheory.volume (parabolicCylinder x t₂ r)
    source
    theorem CKN.Foundation.Parabolic.closedBall_subset_parabolicCylinder {x : Vec3} {t r : ℝ} (hr : 0 < r) :
    Metric.closedBall (x, t) r ⊆ parabolicCylinder x (t + 8 * r ^ 2) (4 * r)
    source
    theorem CKN.Foundation.Parabolic.parabolicCylinder_subset_closedBall {x : Vec3} {t r : ℝ} (hr : 0 < r) :
    parabolicCylinder x (t + r ^ 2 / 2) r ⊆ Metric.closedBall (x, t) r
    source
    theorem CKN.Foundation.Parabolic.volume_parabolicBall_five_mul_le {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) :
    MeasureTheory.volume (Metric.ball z (5 * r)) ≤ ENNReal.ofReal (10 ^ 5) * MeasureTheory.volume (Metric.ball z r)
    source
    theorem CKN.Foundation.Parabolic.volume_parabolicBall_two_mul_le {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) :
    MeasureTheory.volume (Metric.ball z (2 * r)) ≤ ENNReal.ofReal (10 ^ 5) * MeasureTheory.volume (Metric.ball z r)
    source
    theorem CKN.Foundation.Parabolic.volume_parabolicBall_pos {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) :
    0 < MeasureTheory.volume (Metric.ball z r)
    source
    theorem CKN.Foundation.Parabolic.volume_parabolicBall_lt_top {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) :
    MeasureTheory.volume (Metric.ball z r) < ⊤
    source
    instance CKN.Foundation.Parabolic.parabolicVolumeIsUnifLocDoublingMeasure :
    IsUnifLocDoublingMeasure MeasureTheory.volume