Scaling, translation, and radius monotonicity

The declarations here keep the geometric maps from Basic.lean and expose the change-of-variables statements needed for scale-invariant quantities. In particular, no source-facing quantity is introduced in this module.

noncomputable def CKN.Foundation.Parabolic.Integration.parabolicRescale (a κ : ℝ) (x : Vec3) (t : ℝ) (u : ParabolicPoint → ℝ) (p : ParabolicPoint) : ℝ

A parabolic rescaling with a scalar power weight.

Equations

• CKN.Foundation.Parabolic.Integration.parabolicRescale a κ x t u p = a ^ κ * u (CKN.Foundation.Parabolic.parabolicTranslate x t (CKN.Foundation.Parabolic.parabolicScale a p))

theorem CKN.Foundation.Parabolic.Integration.parabolicCylinder_rescale_image {a : ℝ} (ha : 0 < a) (x : Vec3) (t r : ℝ) : parabolicTranslate x t '' parabolicScale a '' parabolicCylinder 0 0 r = parabolicCylinder x t (a * r)

The image of a centred cylinder under a positive rescaling and translation.

theorem CKN.Foundation.Parabolic.Integration.cylinder_setIntegral_comp_parabolicRescale {a : ℝ} (ha : 0 < a) (x : Vec3) (t r : ℝ) (F : ParabolicPoint → ℝ) (hsource : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => F (parabolicTranslate x t (parabolicScale a z))) (parabolicCylinder 0 0 r) MeasureTheory.volume) (htarget : MeasureTheory.IntegrableOn F (parabolicCylinder x t (a * r)) MeasureTheory.volume) : ∫ (z : ParabolicPoint) in parabolicCylinder 0 0 r, F (parabolicTranslate x t (parabolicScale a z)) = a⁻¹ ^ 5 * ∫ (z : ParabolicPoint) in parabolicCylinder x t (a * r), F z

Bochner integration on a parabolic cylinder changes by the homogeneous factor a⁻⁵.

theorem CKN.Foundation.Parabolic.Integration.cylinder_setLIntegral_comp_parabolicRescale {a : ℝ} (ha : 0 < a) (x : Vec3) (t r p : ℝ) (u : ParabolicPoint → ℝ) (hp : 0 ≤ p) (hsource : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u (parabolicTranslate x t (parabolicScale a z))| ^ p) (parabolicCylinder 0 0 r) MeasureTheory.volume) (htarget : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u z| ^ p) (parabolicCylinder x t (a * r)) MeasureTheory.volume) : ∫⁻ (z : ParabolicPoint) in parabolicCylinder 0 0 r, ‖u (parabolicTranslate x t (parabolicScale a z))‖ₑ ^ p = ENNReal.ofReal (a⁻¹ ^ 5) * ∫⁻ (z : ParabolicPoint) in parabolicCylinder x t (a * r), ‖u z‖ₑ ^ p

The corresponding nonnegative cylinder lintegral has homogeneous factor a⁻⁵.

theorem CKN.Foundation.Parabolic.Integration.cylinder_setIntegral_rescaled_power {a : ℝ} (ha : 0 < a) (x : Vec3) (t r p : ℝ) (u : ParabolicPoint → ℝ) (hsource : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u (parabolicTranslate x t (parabolicScale a z))| ^ p) (parabolicCylinder 0 0 r) MeasureTheory.volume) (htarget : MeasureTheory.IntegrableOn (fun (z : ParabolicPoint) => |u z| ^ p) (parabolicCylinder x t (a * r)) MeasureTheory.volume) : ∫ (z : ParabolicPoint) in parabolicCylinder 0 0 r, |a * u (parabolicTranslate x t (parabolicScale a z))| ^ p = a ^ (p - 5) * ∫ (z : ParabolicPoint) in parabolicCylinder x t (a * r), |u z| ^ p

The velocity-weighted cylinder power integral changes by a^(p-5).

theorem CKN.Foundation.Parabolic.Integration.timeSlice_setIntegral_comp_parabolicRescale {a : ℝ} (ha : 0 < a) (x : Vec3) (t r s : ℝ) (F : Vec3 → ℝ) : ∫ (y : Vec3) in vec3Ball 0 r, F (parabolicTranslate x t (parabolicScale a (y, s))).1 = a⁻¹ ^ Module.finrank ℝ Vec3 * ∫ (y : Vec3) in vec3Ball x (a * r), F y

A single spatial time slice changes by the spatial factor a⁻³.

theorem CKN.Foundation.Parabolic.Integration.timeSlice_setIntegral_rescaled_power {a : ℝ} (ha : 0 < a) (x : Vec3) (t r s p : ℝ) (u : ParabolicPoint → ℝ) : MeasureTheory.IntegrableOn (fun (y : Vec3) => |u (parabolicTranslate x t (parabolicScale a (y, s)))| ^ p) (vec3Ball 0 r) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (y : Vec3) => |u (y, t + a ^ 2 * s)| ^ p) (vec3Ball x (a * r)) MeasureTheory.volume → ∫ (y : Vec3) in vec3Ball 0 r, |a * u (parabolicTranslate x t (parabolicScale a (y, s)))| ^ p = a ^ (p - 3) * ∫ (y : Vec3) in vec3Ball x (a * r), |u (y, t + a ^ 2 * s)| ^ p

A velocity-weighted time-slice power integral changes by a^(p-3).

theorem CKN.Foundation.Parabolic.Integration.timeSlice_setLIntegral_comp_parabolicRescale {a : ℝ} (ha : 0 < a) (x : Vec3) (t r s : ℝ) (g : ParabolicPoint → ℝ) : ∫⁻ (y : Vec3) in vec3Ball 0 r, ‖g (parabolicTranslate x t (parabolicScale a (y, s)))‖ₑ ^ 2 = ENNReal.ofReal (a⁻¹ ^ 3) * ∫⁻ (y : Vec3) in vec3Ball x (a * r), ‖g (y, t + a ^ 2 * s)‖ₑ ^ 2

theorem CKN.Foundation.Parabolic.Integration.spatial_setIntegral_comp_smul {a : ℝ} (ha : 0 < a) (x : Vec3) (r : ℝ) (f : Vec3 → ℝ) : ∫ (y : Vec3) in vec3Ball x r, f (a • y) = (a ^ Module.finrank ℝ Vec3)⁻¹ • ∫ (y : Vec3) in a • vec3Ball x r, f y

Spatial change of variables under a positive dilation.

theorem CKN.Foundation.Parabolic.Integration.time_setIntegral_comp_smul {a : ℝ} (ha : 0 < a) (s₁ s₂ : ℝ) (f : ℝ → ℝ) : ∫ (s : ℝ) in Set.Ioc s₁ s₂, f (a • s) = (a ^ Module.finrank ℝ ℝ)⁻¹ • ∫ (s : ℝ) in a • Set.Ioc s₁ s₂, f s

One-dimensional time change of variables under a positive dilation.

theorem CKN.Foundation.Parabolic.Integration.spatial_setIntegral_rescaled_power {a : ℝ} (ha : 0 < a) (x : Vec3) (r p c : ℝ) (u : Vec3 → ℝ) : ∫ (y : Vec3) in vec3Ball x r, |c * u (a • y)| ^ p = (a ^ Module.finrank ℝ Vec3)⁻¹ * ∫ (y : Vec3) in a • vec3Ball x r, |c * u y| ^ p

Spatial power integrals transform with an arbitrary constant weight.

theorem CKN.Foundation.Parabolic.Integration.time_setIntegral_rescaled_power {a : ℝ} (ha : 0 < a) (s₁ s₂ p c : ℝ) (u : ℝ → ℝ) : ∫ (s : ℝ) in Set.Ioc s₁ s₂, |c * u (a • s)| ^ p = (a ^ Module.finrank ℝ ℝ)⁻¹ * ∫ (s : ℝ) in a • Set.Ioc s₁ s₂, |c * u s| ^ p

Time-slice power integrals transform with an arbitrary constant weight.

theorem CKN.Foundation.Parabolic.Integration.volume_parabolicCylinder_translate (a x : Vec3) (τ t r : ℝ) : MeasureTheory.volume (parabolicCylinder (a + x) (τ + t) r) = MeasureTheory.volume (parabolicCylinder x t r)

Translation preserves the volume of a parabolic cylinder.

noncomputable def CKN.Foundation.Parabolic.Integration.timeSliceBallEnergy (x : Vec3) (r s : ℝ) (g : ParabolicPoint → ℝ) : ENNReal

The nonnegative energy of a spatial time slice.

Equations

• CKN.Foundation.Parabolic.Integration.timeSliceBallEnergy x r s g = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x r, ‖g (y, s)‖ₑ ^ 2

noncomputable def CKN.Foundation.Parabolic.Integration.timeSliceEnergyEssSup (x : Vec3) (t r : ℝ) (g : ParabolicPoint → ℝ) : ENNReal

Essential supremum of a time-slice energy over the cylinder time interval.

Equations

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

theorem CKN.Foundation.Parabolic.Integration.timeSliceEnergyEssSup_comp_parabolicRescale {a : ℝ} (ha : 0 < a) (x : Vec3) (t r : ℝ) (g : ParabolicPoint → ℝ) (hsource : Filter.IsBoundedUnder (fun (x1 x2 : ENNReal) => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.volume.restrict (Set.Ioc (-r ^ 2) 0))) fun (s : ℝ) => ∫⁻ (y : Vec3) in vec3Ball x (a * r), ‖g (y, t + a ^ 2 * s)‖ₑ ^ 2) (htarget : Filter.IsBoundedUnder (fun (x1 x2 : ENNReal) => x1 ≤ x2) (MeasureTheory.ae (MeasureTheory.volume.restrict (Set.Ioc (t - (a * r) ^ 2) t))) fun (s : ℝ) => ∫⁻ (y : Vec3) in vec3Ball x (a * r), ‖g (y, s)‖ₑ ^ 2) : (timeSliceEnergyEssSup 0 0 r fun (z : ParabolicPoint) => g (parabolicTranslate x t (parabolicScale a z))) = ENNReal.ofReal (a⁻¹ ^ 3) * timeSliceEnergyEssSup x t (a * r) g

The time-slice energy essential supremum changes by the spatial factor a⁻³.

theorem CKN.Foundation.Parabolic.Integration.essSup_mono_measure_and_ae {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f g : α → ENNReal} (hμν : μ ≤ ν) (hfg : f ≤ᵐ[μ] g) : essSup f μ ≤ essSup g ν

Essential suprema increase when the measure and the integrand both increase.

theorem CKN.Foundation.Parabolic.Integration.time_interval_mono_radius {t r₁ r₂ : ℝ} (hr₁ : 0 ≤ r₁) (hrr : r₁ ≤ r₂) : Set.Ioc (t - r₁ ^ 2) t ⊆ Set.Ioc (t - r₂ ^ 2) t

The time interval for a smaller nonnegative radius is contained in the larger one.

theorem CKN.Foundation.Parabolic.Integration.timeSliceEnergyEssSup_mono_radius {x : Vec3} {t r₁ r₂ : ℝ} (hr₁ : 0 ≤ r₁) (hrr : r₁ ≤ r₂) (g : ParabolicPoint → ℝ) : timeSliceEnergyEssSup x t r₁ g ≤ timeSliceEnergyEssSup x t r₂ g

The time-slice L² energy essential supremum is monotone in the radius.

theorem CKN.Foundation.Parabolic.Integration.timeSliceEnergyEssSup_div_radius_le {x : Vec3} {t r₁ r₂ : ℝ} (hr₁ : 0 < r₁) (hrr : r₁ ≤ r₂) (g : ParabolicPoint → ℝ) : timeSliceEnergyEssSup x t r₁ g / ENNReal.ofReal r₁ ≤ ENNReal.ofReal (r₂ / r₁) * (timeSliceEnergyEssSup x t r₂ g / ENNReal.ofReal r₂)

The radius-normalized time-slice essential supremum has the standard comparison.