Almost-everywhere bookkeeping for the rescaled trace

The blow-up sequence of prop:blowup-limit is built from the jointly measurable trace representative of lem:weak-cont-L3. These lemmas move almost-everywhere statements between time slices and space-time, and pull them back through the parabolic rescaling.

theorem ESS.blowupLimitAssembly_ae_ae_of_ae_prod_swap {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {p : α × β → Prop} (h : ∀ᵐ (z : α × β) ∂μ.prod ν, p z) : ∀ᵐ (y : β) ∂ν, ∀ᵐ (x : α) ∂μ, p (x, y)

Almost every point of a product measure gives, for almost every second coordinate, almost every first coordinate.

theorem ESS.blowupLimitAssembly_ae_slices_of_ae_spaceTime {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {p : CKN.Foundation.Parabolic.ParabolicPoint → Prop} (h : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω I), p z) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict Ω, p (x, t)

A space-time almost-everywhere property on a product cylinder holds, for almost every time, almost everywhere on the spatial slice.

theorem ESS.blowupLimitAssembly_ae_eq_of_ae_slices {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {F G : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hF : Measurable F) (hG : Measurable G) (h : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict Ω, F (x, t) = G (x, t)) : F =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω I)] G

Slicewise almost-everywhere equality of measurable fields is space-time almost-everywhere equality.

theorem ESS.blowupLimitAssembly_ae_rescale_pullback (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : MeasurableSet Ω) (hI : MeasurableSet I) {p : CKN.Foundation.Parabolic.ParabolicPoint → Prop} (h : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω I), p z) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.rescaledSpace r x₀ Ω) (CKN.rescaledTime r t₀ I)), p (CKN.Foundation.Parabolic.parabolicTranslate x₀ t₀ (CKN.Foundation.Parabolic.parabolicScale r z))

A space-time almost-everywhere property pulls back through a positive parabolic rescaling.

theorem ESS.blowupLimitAssembly_scalingSpace_image_vec3Ball (x₀ : CKN.Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (R : ℝ) : CKN.scalingSpace r x₀ '' CKN.Foundation.Parabolic.vec3Ball 0 R = CKN.Foundation.Parabolic.vec3Ball x₀ (r * R)

The spatial rescaling maps a centred ball onto a ball around the base point.

theorem ESS.blowupLimitAssembly_hasWeakPartialDerivOn_congr {Ω : Set CKN.Foundation.Parabolic.Vec3} {i : Fin 3} {u u' g g' : CKN.Foundation.Parabolic.Vec3 → ℝ} (hu : u =ᵐ[MeasureTheory.volume.restrict Ω] u') (hg : g =ᵐ[MeasureTheory.volume.restrict Ω] g') (h : CKN.HasWeakPartialDerivOn Ω i u g) : CKN.HasWeakPartialDerivOn Ω i u' g'

Weak partial derivatives are unchanged by almost-everywhere changes on the domain.

theorem ESS.blowupLimitAssembly_traceZeroExtension_ae_eq {u um : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hum : Measurable um) (hu : u =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))] um) (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3) (hW : Measurable W) (htrace : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0), (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, ⟨t, ht⟩)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))] fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) : blowupLimitTraceZeroExtension W =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-(3 / 4) ^ 2) 0))] u

The zero-extended trace representative agrees almost everywhere with the source velocity on the inner source cylinder.