Scaling Invariance Tests

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

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

Spatial scaling homeomorphism used to differentiate pulled-back test functions.

Equations

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

theorem CKN.spatialPartial_pullback (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : spatialPartial (ψ ∘ fun (w : Foundation.Parabolic.ParabolicPoint) => (μ⁻¹ • (w.1 - z₀.1), (μ ^ 2)⁻¹ * (w.2 - z₀.2))) j (scalingParabolic μ z₀ z) = μ⁻¹ * spatialPartial ψ j z

theorem CKN.timePartial_pullback (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (z : Foundation.Parabolic.ParabolicPoint) : timePartial (ψ ∘ fun (w : Foundation.Parabolic.ParabolicPoint) => (μ⁻¹ • (w.1 - z₀.1), (μ ^ 2)⁻¹ * (w.2 - z₀.2))) (scalingParabolic μ z₀ z) = (μ ^ 2)⁻¹ * timePartial ψ z

theorem CKN.spatialSecondPartial_pullback (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) : spatialSecondPartial (ψ ∘ fun (w : Foundation.Parabolic.ParabolicPoint) => (μ⁻¹ • (w.1 - z₀.1), (μ ^ 2)⁻¹ * (w.2 - z₀.2))) i j (scalingParabolic μ z₀ z) = (μ ^ 2)⁻¹ * spatialSecondPartial ψ i j z

theorem CKN.integral_comp_scaling_test (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hΩ : MeasurableSet Ω) (hI : MeasurableSet I) (hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (spaceTimeSet Ω I))) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I), F (scalingParabolic μ z₀ z) = (ENNReal.ofReal (μ⁻¹ ^ 5)).toReal • ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, F z

theorem CKN.integrable_comp_scaling_test (μ : ℝ) (hμ : 0 < μ) (z₀ : Foundation.Parabolic.ParabolicPoint) {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hΩ : MeasurableSet Ω) (hI : MeasurableSet I) (hF : MeasureTheory.IntegrableOn F (spaceTimeSet Ω I) MeasureTheory.volume) : MeasureTheory.IntegrableOn (F ∘ scalingParabolic μ z₀) (spaceTimeSet (rescaledSpace μ z₀.1 Ω) (rescaledTime μ z₀.2 I)) MeasureTheory.volume

theorem CKN.spatialPartial_zero_of_not_mem_tsupport_public {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) (i : Fin 3) : spatialPartial ψ i z = 0

theorem CKN.timePartial_zero_of_not_mem_tsupport_public {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) : timePartial ψ z = 0

theorem CKN.spatialSecondPartial_zero_of_not_mem_tsupport_public {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) (i j : Fin 3) : spatialSecondPartial ψ i j z = 0