The parabolic rescaling as a change of variables

The parabolic rescaling (y, s) ↦ (x₀ + μ y, t₀ + μ² s) is a homeomorphism of space-time whose Jacobian is the constant μ⁵. This file records what is needed to move a statement proved on the unit cylinder to a statement on the cylinder B(x₀, μ) × (t₀ - μ², t₀]: the preimage of a parabolic cylinder, the change of variables for lower Lebesgue integrals, and the transport of an almost-everywhere statement. A last lemma assembles almost-everywhere bounds on a countable family of sets into one bound on a set that the family covers.

theorem CIV.measurableEmbedding_scalingParabolic {μ : ℝ} (hμ : 0 < μ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) : MeasurableEmbedding (CKN.scalingParabolic μ z₀)

The parabolic rescaling is a measurable embedding.

theorem CIV.measurable_scalingParabolic {μ : ℝ} (hμ : 0 < μ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) : Measurable (CKN.scalingParabolic μ z₀)

The parabolic rescaling is measurable.

theorem CIV.mem_parabolicCylinder_iff (x : CKN.Foundation.Parabolic.Vec3) (t r : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : z ∈ CKN.Foundation.Parabolic.parabolicCylinder x t r ↔ CKN.Foundation.Parabolic.vec3EuclideanNorm (z.1 - x) < r ∧ t - r ^ 2 < z.2 ∧ z.2 ≤ t

Membership in a parabolic cylinder, read on the components of a space-time point.

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

A parabolic cylinder is measurable.

theorem CIV.preimage_scalingParabolic_parabolicCylinder {μ : ℝ} (hμ : 0 < μ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) (r : ℝ) : CKN.scalingParabolic μ z₀ ⁻¹' CKN.Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 (μ * r) = CKN.Foundation.Parabolic.parabolicCylinder 0 0 r

The rescaling carries the cylinder of radius r at the origin onto the cylinder of radius μ r at z₀.

theorem CIV.map_scalingParabolic_restrict_preimage {μ : ℝ} (hμ : 0 < μ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) : MeasureTheory.Measure.map (CKN.scalingParabolic μ z₀) (MeasureTheory.volume.restrict (CKN.scalingParabolic μ z₀ ⁻¹' S)) = ENNReal.ofReal (μ⁻¹ ^ 5) • MeasureTheory.volume.restrict S

The rescaling pushes the measure restricted to a preimage forward to a multiple of the measure restricted to the set.

theorem CIV.setLIntegral_comp_scalingParabolic {μ : ℝ} (hμ : 0 < μ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) (F : CKN.Foundation.Parabolic.ParabolicPoint → ENNReal) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.scalingParabolic μ z₀ ⁻¹' S, F (CKN.scalingParabolic μ z₀ z) = ENNReal.ofReal (μ⁻¹ ^ 5) * ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, F z

Change of variables for a lower Lebesgue integral along the parabolic rescaling: no measurability of the integrand is needed, because the rescaling is a measurable embedding.

theorem CIV.ae_restrict_of_ae_restrict_comp_scalingParabolic {μ : ℝ} (hμ : 0 < μ) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) {P : CKN.Foundation.Parabolic.ParabolicPoint → Prop} (h : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.scalingParabolic μ z₀ ⁻¹' S), P (CKN.scalingParabolic μ z₀ z)) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict S, P z

An almost-everywhere statement on the preimage of a set transports to the set itself.

theorem CIV.ae_restrict_of_countable_cover {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.Measure α} {ι : Type u_2} {J : Set ι} (hJ : J.Countable) {A : ι → Set α} {U : Set α} (hU : MeasurableSet U) (hA : ∀ i ∈ J, MeasurableSet (A i)) (hcover : U ⊆ ⋃ i ∈ J, A i) {P : α → Prop} (h : ∀ i ∈ J, ∀ᵐ (z : α) ∂m.restrict (A i), P z) : ∀ᵐ (z : α) ∂m.restrict U, P z

Almost-everywhere bounds on a countable family of measurable sets give an almost-everywhere bound on any measurable set the family covers.