Changes of variables under parabolic scaling

The parabolic scaling z ↦ (x₀ + R x, t₀ + R² t) is a measurable equivalence of space-time whose push-forward of Lebesgue measure is R⁻⁵ times Lebesgue measure. This file records the resulting change-of-variables identities for lower integrals, almost-everywhere statements, measurability and Lᵖ membership, with no measurability hypothesis on lower integrands. They are the bookkeeping behind the rescaling step of lem:pv-positive-bound.

noncomputable def ESS.pvScalingEquiv (R : ℝ) (hR : 0 < R) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.ParabolicPoint ≃ᵐ CKN.Foundation.Parabolic.ParabolicPoint

The parabolic scaling map as a measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ESS.pvSpaceScalingEquiv (R : ℝ) (hR : 0 < R) (x₀ : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3 ≃ᵐ CKN.Foundation.Parabolic.Vec3

The spatial scaling map as a measurable equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.pv_lintegral_scalingParabolic (R : ℝ) (hR : 0 < R) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (F : CKN.Foundation.Parabolic.ParabolicPoint → ENNReal) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.scalingParabolic R z₀ ⁻¹' S, F (CKN.scalingParabolic R z₀ z) = ENNReal.ofReal (R⁻¹ ^ 5) * ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, F z

Change of variables for lower integrals under parabolic scaling, for an arbitrary integrand and an arbitrary target set.

theorem ESS.pv_lintegral_scalingSpace (R : ℝ) (hR : 0 < R) (x₀ : CKN.Foundation.Parabolic.Vec3) (A : Set CKN.Foundation.Parabolic.Vec3) (F : CKN.Foundation.Parabolic.Vec3 → ENNReal) : ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.scalingSpace R x₀ ⁻¹' A, F (CKN.scalingSpace R x₀ x) = ENNReal.ofReal (R⁻¹ ^ 3) * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in A, F x

Change of variables for lower integrals under spatial scaling.

theorem ESS.pv_ae_scalingParabolic_iff (R : ℝ) (hR : 0 < R) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (P : CKN.Foundation.Parabolic.ParabolicPoint → Prop) : (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.scalingParabolic R z₀ ⁻¹' S), P (CKN.scalingParabolic R z₀ z)) ↔ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict S, P z

Almost-everywhere statements transfer through parabolic scaling.

theorem ESS.pv_aestronglyMeasurable_comp_scalingParabolic {E : Type} [TopologicalSpace E] (R : ℝ) (hR : 0 < R) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) {S : Set CKN.Foundation.Parabolic.ParabolicPoint} {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict S)) : MeasureTheory.AEStronglyMeasurable (f ∘ CKN.scalingParabolic R z₀) (MeasureTheory.volume.restrict (CKN.scalingParabolic R z₀ ⁻¹' S))

Almost-everywhere strong measurability transfers through parabolic scaling.

theorem ESS.pv_memLp_comp_scalingParabolic {E : Type} [NormedAddCommGroup E] (R : ℝ) (hR : 0 < R) (z₀ : CKN.Foundation.Parabolic.ParabolicPoint) {S : Set CKN.Foundation.Parabolic.ParabolicPoint} {f : CKN.Foundation.Parabolic.ParabolicPoint → E} {q : ENNReal} (hf : MeasureTheory.MemLp f q (MeasureTheory.volume.restrict S)) : MeasureTheory.MemLp (f ∘ CKN.scalingParabolic R z₀) q (MeasureTheory.volume.restrict (CKN.scalingParabolic R z₀ ⁻¹' S))

Lᵖ membership transfers through parabolic scaling.