Scaling Invariance Basic

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

def CKN.scalingSpace (μ : ℝ) (x₀ : Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

Spatial part of the parabolic change of variables.

Equations

• CKN.scalingSpace μ x₀ y = x₀ + μ • y

def CKN.scalingTime (μ t₀ : ℝ) : ℝ → ℝ

Temporal part of the parabolic change of variables.

Equations

• CKN.scalingTime μ t₀ s = t₀ + μ ^ 2 * s

def CKN.scalingParabolic (μ : ℝ) (z₀ : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.ParabolicPoint

Parabolic dilation followed by space-time translation.

Equations

• CKN.scalingParabolic μ z₀ z = CKN.Foundation.Parabolic.parabolicTranslate z₀.1 z₀.2 (CKN.Foundation.Parabolic.parabolicScale μ z)

def CKN.rescaledSpace (μ : ℝ) (x₀ : Foundation.Parabolic.Vec3) (Ω : Set Foundation.Parabolic.Vec3) : Set Foundation.Parabolic.Vec3

Spatial domain pulled back under the parabolic change of variables.

Equations

• CKN.rescaledSpace μ x₀ Ω = CKN.scalingSpace μ x₀ ⁻¹' Ω

def CKN.rescaledTime (μ t₀ : ℝ) (I : Set ℝ) : Set ℝ

Time domain pulled back under the parabolic change of variables.

Equations

• CKN.rescaledTime μ t₀ I = CKN.scalingTime μ t₀ ⁻¹' I

theorem CKN.scalingParabolic_eq (μ : ℝ) (z₀ : Foundation.Parabolic.ParabolicPoint) : scalingParabolic μ z₀ = fun (z : Foundation.Parabolic.ParabolicPoint) => (scalingSpace μ z₀.1 z.1, scalingTime μ z₀.2 z.2)

theorem CKN.rescaledSpaceTimeSet_eq_preimage (μ : ℝ) (z₀ : Foundation.Parabolic.ParabolicPoint) (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) : spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I) = scalingParabolic μ z₀ ⁻¹' spaceTimeSet Ω I

theorem CKN.rescaledSpace_isOpen {μ : ℝ} (x₀ : Foundation.Parabolic.Vec3) {Ω : Set Foundation.Parabolic.Vec3} (hΩ : IsOpen Ω) : IsOpen (rescaledSpace μ x₀ Ω)

theorem CKN.rescaledTime_isOpen {μ : ℝ} (t₀ : ℝ) {I : Set ℝ} (hI : IsOpen I) : IsOpen (rescaledTime μ t₀ I)

theorem CKN.rescaledTime_ordConnected {μ : ℝ} : 0 < μ → ∀ (t₀ : ℝ) {I : Set ℝ} (hI : I.OrdConnected), (rescaledTime μ t₀ I).OrdConnected

noncomputable def CKN.scalingSpaceHomeomorph (μ : ℝ) (hμ : 0 < μ) (x₀ : Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 ≃ₜ Foundation.Parabolic.Vec3

Homeomorphism underlying the spatial scaling map.

Equations

• CKN.scalingSpaceHomeomorph μ hμ x₀ = (Homeomorph.smulOfNeZero μ ⋯).trans (Homeomorph.addLeft x₀)

noncomputable def CKN.scalingTimeHomeomorph (μ : ℝ) (hμ : 0 < μ) (t₀ : ℝ) : ℝ ≃ₜ ℝ

Homeomorphism underlying the temporal scaling map.

Equations

• CKN.scalingTimeHomeomorph μ hμ t₀ = (Homeomorph.smulOfNeZero (μ ^ 2) ⋯).trans (Homeomorph.addLeft t₀)

noncomputable def CKN.scalingTimeInv (μ t₀ : ℝ) : ℝ → ℝ

Inverse temporal affine map used in scaling the weak equations.

Equations

• CKN.scalingTimeInv μ t₀ s = (μ ^ 2)⁻¹ * (s - t₀)

theorem CKN.map_scalingSpace (μ : ℝ) (hμ : 0 < μ) (x₀ : Foundation.Parabolic.Vec3) : MeasureTheory.Measure.map (scalingSpace μ x₀) MeasureTheory.volume = ENNReal.ofReal (μ⁻¹ ^ 3) • MeasureTheory.volume

theorem CKN.map_scalingTime (μ : ℝ) (hμ : 0 < μ) (t₀ : ℝ) : MeasureTheory.Measure.map (scalingTime μ t₀) MeasureTheory.volume = ENNReal.ofReal (μ ^ 2)⁻¹ • MeasureTheory.volume

theorem CKN.map_scalingParabolic (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) : MeasureTheory.Measure.map (scalingParabolic μ z₀) MeasureTheory.volume = ENNReal.ofReal (μ⁻¹ ^ 5) • MeasureTheory.volume

theorem CKN.map_scalingSpace_restrict {μ : ℝ} (hμ : 0 < μ) (x₀ : Foundation.Parabolic.Vec3) {Ω : Set Foundation.Parabolic.Vec3} (hΩ : MeasurableSet Ω) : MeasureTheory.Measure.map (scalingSpace μ x₀) (MeasureTheory.volume.restrict (rescaledSpace μ x₀ Ω)) = ENNReal.ofReal (μ⁻¹ ^ 3) • MeasureTheory.volume.restrict Ω

theorem CKN.map_scalingTime_restrict {μ : ℝ} (hμ : 0 < μ) (t₀ : ℝ) {I : Set ℝ} (hI : MeasurableSet I) : MeasureTheory.Measure.map (scalingTime μ t₀) (MeasureTheory.volume.restrict (rescaledTime μ t₀ I)) = ENNReal.ofReal (μ ^ 2)⁻¹ • MeasureTheory.volume.restrict I

theorem CKN.map_scalingParabolic_restrict {μ : ℝ} (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : MeasurableSet Ω) (hI : MeasurableSet I) : MeasureTheory.Measure.map (scalingParabolic μ z₀) (MeasureTheory.volume.restrict (spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I))) = ENNReal.ofReal (μ⁻¹ ^ 5) • MeasureTheory.volume.restrict (spaceTimeSet Ω I)

theorem CKN.localBox_forward {μ : ℝ} (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I) Ω' J) : localBox Ω I (scalingSpace μ z₀.1 '' Ω') (scalingTime μ z₀.2 '' J)