Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.EssLocalProofVorticity

Ess Local Proof Vorticity #

Local endpoint regularity through vorticity estimates and backward uniqueness.

source
noncomputable def ESS.essLocalTimeReflection :
CKN.Foundation.Parabolic.ParabolicPoint ≃ₜ CKN.Foundation.Parabolic.ParabolicPoint

Reflection of the time coordinate in the terminal face.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem ESS.essLocalTimeReflection_apply (z : CKN.Foundation.Parabolic.ParabolicPoint) :
    essLocalTimeReflection z = (z.1, -z.2)
    source
    noncomputable def ESS.essLocalSpatialTranslate (c : CKN.Foundation.Parabolic.Vec3) :
    CKN.Foundation.Parabolic.ParabolicPoint ≃ₜ CKN.Foundation.Parabolic.ParabolicPoint

    Translation of the spatial coordinate in parabolic space-time.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem ESS.essLocalSpatialTranslate_apply (c : CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
      (essLocalSpatialTranslate c) z = (c + z.1, z.2)
      source
      noncomputable def ESS.essLocalTimeTranslate (d : ℝ) :
      CKN.Foundation.Parabolic.ParabolicPoint ≃ₜ CKN.Foundation.Parabolic.ParabolicPoint

      Translation of the time coordinate in parabolic space-time.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem ESS.essLocalTimeTranslate_apply (d : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
        (essLocalTimeTranslate d) z = (z.1, d + z.2)
        source
        theorem ESS.essLocalSpatialTranslate_measurePreserving (c : CKN.Foundation.Parabolic.Vec3) :
        MeasureTheory.MeasurePreserving (⇑(essLocalSpatialTranslate c)) MeasureTheory.volume MeasureTheory.volume

        Spatial translation preserves parabolic space-time volume.

        source
        theorem ESS.essLocalTimeTranslate_measurePreserving (d : ℝ) :
        MeasureTheory.MeasurePreserving (⇑(essLocalTimeTranslate d)) MeasureTheory.volume MeasureTheory.volume

        Time translation preserves parabolic space-time volume.

        source
        theorem ESS.essLocalTimeReflection_measurePreserving :
        MeasureTheory.MeasurePreserving (⇑essLocalTimeReflection) MeasureTheory.volume MeasureTheory.volume

        Reflection of time preserves parabolic space-time volume.

        source
        theorem ESS.essLocalTimeReflection_image (Ω : Set CKN.Foundation.Parabolic.Vec3) (T : ℝ) :
        ⇑essLocalTimeReflection '' CKN.spaceTimeSet Ω (Set.Ioo 0 T) = CKN.spaceTimeSet Ω (Set.Ioo (-T) 0)

        Time reflection sends a positive interval to the corresponding past interval.

        source
        theorem ESS.essLocal_weakDerivs_restrict {Ω Ω' : Set CKN.Foundation.Parabolic.Vec3} {I J : Set ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hΩ : Ω' ⊆ Ω) (hJ : J ⊆ I) (hQmeas : MeasurableSet (CKN.spaceTimeSet Ω I)) (hweak : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) :
        CKN.HasSpaceTimeWeakDerivs Ω' J w Dw D2w Dtw

        Space-time weak derivatives restrict to a smaller open spatial and time domain.

        source
        theorem ESS.essLocal_spatialTranslate_weakDerivs {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (c : CKN.Foundation.Parabolic.Vec3) (hΩ : IsOpen Ω) (hI : IsOpen I) (hweak : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) :
        CKN.HasSpaceTimeWeakDerivs {y : CKN.Foundation.Parabolic.Vec3 | c + y ∈ Ω} I (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => w ((essLocalSpatialTranslate c) z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => Dw ((essLocalSpatialTranslate c) z) i j) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => D2w ((essLocalSpatialTranslate c) z) i j k) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Dtw ((essLocalSpatialTranslate c) z) i

        Space-time weak derivatives transport under spatial translation.

        source
        theorem ESS.essLocal_timeTranslate_weakDerivs {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (d : ℝ) (hΩ : IsOpen Ω) (hI : IsOpen I) (hweak : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) :
        CKN.HasSpaceTimeWeakDerivs Ω {s : ℝ | s + d ∈ I} (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => w ((essLocalTimeTranslate d) z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => Dw ((essLocalTimeTranslate d) z) i j) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => D2w ((essLocalTimeTranslate d) z) i j k) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => Dtw ((essLocalTimeTranslate d) z) i

        Space-time weak derivatives transport under time translation.

        source
        theorem ESS.essLocal_timeReflection_weakDerivs {Ω : Set CKN.Foundation.Parabolic.Vec3} {T : ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) (hweak : CKN.HasSpaceTimeWeakDerivs Ω (Set.Ioo (-T) 0) w Dw D2w Dtw) :
        CKN.HasSpaceTimeWeakDerivs Ω (Set.Ioo 0 T) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => w (essLocalTimeReflection z)) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => Dw (essLocalTimeReflection z) i j) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => D2w (essLocalTimeReflection z) i j k) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => -Dtw (essLocalTimeReflection z) i

        Distributional spatial and time derivatives transport across reflection of the terminal face.

        source
        theorem ESS.essLocal_scale_weakDerivs {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (a : ℝ) (hweak : CKN.HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) :
        CKN.HasSpaceTimeWeakDerivs Ω I (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => a • w z) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => a * Dw z i j) (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => a * D2w z i j k) fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => a * Dtw z i

        Multiplying a field and each of its weak derivatives by the same real constant preserves the space-time weak-derivative identities.