Param Extension

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

noncomputable def CKN.parametricPairing {X : Type} (Ψ : X → Foundation.Parabolic.Vec3 → ℝ) (g₀ : Foundation.Parabolic.Vec3 → ℝ) (g₁ : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (g₂ : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ) (x : X) : ℝ

The scalar pairing of a parameterized test family with zeroth, first, and second order slice data on a fixed compact set.

Equations

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

theorem CKN.continuous_parametricPairing {X : Type} [TopologicalSpace X] {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (Ψ : X → Foundation.Parabolic.Vec3 → ℝ) (g₀ : Foundation.Parabolic.Vec3 → ℝ) (g₁ : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (g₂ : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ) (hΨ₀ : Continuous fun (z : X × Foundation.Parabolic.Vec3) => Ψ z.1 z.2) (hΨ₁ : ∀ (i : Fin 3), Continuous fun (z : X × Foundation.Parabolic.Vec3) => spatialDeriv (Ψ z.1) i z.2) (hΨ₂ : ∀ (i j : Fin 3), Continuous fun (z : X × Foundation.Parabolic.Vec3) => mixedSecond (Ψ z.1) i j z.2) (hK₀ : ∀ (x : X), ∀ y ∉ K, Ψ x y = 0) (hK₁ : ∀ (x : X) (y : Foundation.Parabolic.Vec3) (i : Fin 3), y ∉ K → spatialDeriv (Ψ x) i y = 0) (hK₂ : ∀ (x : X) (y : Foundation.Parabolic.Vec3) (i j : Fin 3), y ∉ K → mixedSecond (Ψ x) i j y = 0) (hg₀ : MeasureTheory.IntegrableOn g₀ K MeasureTheory.volume) (hg₁ : MeasureTheory.IntegrableOn g₁ K MeasureTheory.volume) (hg₂ : MeasureTheory.IntegrableOn g₂ K MeasureTheory.volume) : Continuous (parametricPairing Ψ g₀ g₁ g₂)

A fixed compact support and joint continuity through second order make the parameterized slice pairing continuous.

theorem CKN.parametricPairing_eq_zero_of_dense {X : Type} [TopologicalSpace X] {Ψ : X → Foundation.Parabolic.Vec3 → ℝ} {g₀ : Foundation.Parabolic.Vec3 → ℝ} {g₁ : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {g₂ : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ} {D : Set X} (hD : Dense D) (hcont : Continuous (parametricPairing Ψ g₀ g₁ g₂)) (hzero : ∀ x ∈ D, parametricPairing Ψ g₀ g₁ g₂ x = 0) (x : X) : parametricPairing Ψ g₀ g₁ g₂ x = 0

A continuous scalar pairing which vanishes on a dense parameter set vanishes for every parameter.

theorem CKN.parametricPairing_eq_zero_of_countable_dense {X : Type} [TopologicalSpace X] {Ψ : X → Foundation.Parabolic.Vec3 → ℝ} {g₀ : Foundation.Parabolic.Vec3 → ℝ} {g₁ : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {g₂ : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ} {D : Set X} : D.Countable → ∀ (hD : Dense D) (hcont : Continuous (parametricPairing Ψ g₀ g₁ g₂)) (hzero : ∀ x ∈ D, parametricPairing Ψ g₀ g₁ g₂ x = 0) (x : X), parametricPairing Ψ g₀ g₁ g₂ x = 0

A continuous scalar pairing which vanishes on a countable dense parameter set vanishes for every parameter.