Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.LocalTimeProjection

Time projections of the singular set #

This file proves the projection and regular-neighborhood conclusions of lem:time-projection.

source
def ESS.parabolicTimeProjection (S : Set CKN.Foundation.Parabolic.ParabolicPoint) :
Set ℝ

The time-coordinate projection of a parabolic set.

Equations
Instances For
    source
    theorem ESS.parabolicTimeProjection_null_of_hausdorffMeasure_zero (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (hS : (CKN.Foundation.Parabolic.parabolicHausdorffMeasure 1) S = 0) :
    MeasureTheory.volume (parabolicTimeProjection S) = 0

    A zero one-dimensional parabolic Hausdorff measure has a Lebesgue-null time projection.

    source
    def ESS.regularPointLocus (I : Set ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) :
    Set CKN.Foundation.Parabolic.ParabolicPoint

    The set of CKN regular points in a full spatial domain.

    Equations
    Instances For
      source
      theorem ESS.isOpen_regularPointLocus (I : Set ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) :
      IsOpen (regularPointLocus I u)

      The regular-point locus is open because a Hölder representative on a neighborhood remains a witness at each point of that neighborhood.

      source
      theorem ESS.exists_regularTimeNeighborhood_of_time_not_singular (I : Set ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t ρ : ℝ) (hρ : 0 < ρ) (ht : t ∈ I) (htSing : t ∉ parabolicTimeProjection (CKN.SingularSet Set.univ I u)) :
      ∃ δ > 0, closure (CKN.Foundation.Parabolic.vec3Ball 0 ρ) ×ˢ Set.Ioo (t - δ) (t + δ) ⊆ regularPointLocus I u

      A compact spatial slice disjoint from the singular set has a time collar contained in the regular-point locus.

      source
      theorem ESS.timeProjection_regularNeighborhoods_of_suitable (I : Set ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hSuitable : CKN.IsSuitableWeakSolution Set.univ I 3 u Du p 0) :
      ∀ᵐ (t : ℝ), t ∈ I → ∀ (ρ : ℝ), 0 < ρ → ∃ δ > 0, closure (CKN.Foundation.Parabolic.vec3Ball 0 ρ) ×ˢ Set.Ioo (t - δ) (t + δ) ⊆ regularPointLocus I u

      For an exponent-three suitable solution with zero force on all of space, almost every time has a regular neighborhood around every fixed compact ball.