Density extension for weighted Carleman inequalities

This module is intended to extend smooth compactly supported inequalities to fields with space-time weak derivatives (lem:carleman-sobolev of the Escauriaza–Seregin–Šverák manuscript).

noncomputable def CKN.zeroExtendField {E V : Type} [Zero V] (U : Set E) (f : E → V) : E → V

The pointwise zero extension of a field from a set.

Equations

• CKN.zeroExtendField U f z = if z ∈ U then f z else 0

theorem CKN.zeroExtend_eq_of_tsupport_subset {E V : Type} [Zero V] [TopologicalSpace E] (U : Set E) (f : E → V) (hfsupport : tsupport f ⊆ U) : zeroExtendField U f = f

If a field has support inside U, its pointwise zero extension from U is the field itself. This is the support fact used when extending the weak derivative identities in lem:carleman-sobolev (ESS).

theorem CKN.locallyIntegrableOn_parabolic_to_product {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {E : Type u_1} [NormedAddCommGroup E] {f : Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.LocallyIntegrableOn f (spaceTimeSet Ω I) MeasureTheory.volume) : MeasureTheory.LocallyIntegrableOn (fun (q : Foundation.Parabolic.Vec3 × ℝ) => f (Foundation.Parabolic.parabolicHomeomorph.symm q)) (Ω ×ˢ I) MeasureTheory.volume

Local integrability on a CKN space-time product transfers to its product coordinates.

theorem CKN.setLIntegral_parabolic_to_product {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {F : Foundation.Parabolic.ParabolicPoint → ENNReal} : ∫⁻ (p : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, F p = ∫⁻ (q : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, F (Foundation.Parabolic.parabolicHomeomorph.symm q)

Nonnegative set integrals on a space-time product agree in CKN and product coordinates.

theorem CKN.weak_spatial_identity_product {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφU : tsupport φ ⊆ Ω ×ˢ I) (i j : Fin 3) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, w (Foundation.Parabolic.parabolicHomeomorph.symm y) i * (fderiv ℝ φ y) (basisVec j, 0) = -∫ (y : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, Dw (Foundation.Parabolic.parabolicHomeomorph.symm y) i j * φ y

The weak spatial integration-by-parts identity in product coordinates (lem:carleman-sobolev, ESS).

theorem CKN.weak_spatialSecond_identity_product {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφU : tsupport φ ⊆ Ω ×ˢ I) (i j k : Fin 3) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, Dw (Foundation.Parabolic.parabolicHomeomorph.symm y) i j * (fderiv ℝ φ y) (basisVec k, 0) = -∫ (y : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, D2w (Foundation.Parabolic.parabolicHomeomorph.symm y) i j k * φ y

The weak second spatial integration-by-parts identity in product coordinates (lem:carleman-sobolev, ESS).

theorem CKN.weak_time_identity_product {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hφU : tsupport φ ⊆ Ω ×ˢ I) (i : Fin 3) : ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, w (Foundation.Parabolic.parabolicHomeomorph.symm y) i * (fderiv ℝ φ y) (0, 1) = -∫ (y : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, Dtw (Foundation.Parabolic.parabolicHomeomorph.symm y) i * φ y

The weak time integration-by-parts identity in product coordinates (lem:carleman-sobolev, ESS).

theorem CKN.field_component_ae_zero_off_support {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (i : Fin 3) : ∀ᵐ (y : Foundation.Parabolic.Vec3 × ℝ), y ∈ Ω ×ˢ I → y ∉ ⇑Foundation.Parabolic.parabolicHomeomorph '' tsupport w → w (Foundation.Parabolic.parabolicHomeomorph.symm y) i = 0

A component of a compactly supported field vanishes outside its closed support.

theorem CKN.spaceTimeWeakDerivs_ae_zero_off_tsupport {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) (hcompact : HasCompactSupport w) (htsupport : tsupport w ⊆ spaceTimeSet Ω I) : (∀ (i j : Fin 3), ∀ᵐ (y : Foundation.Parabolic.Vec3 × ℝ), y ∈ Ω ×ˢ I → y ∉ ⇑Foundation.Parabolic.parabolicHomeomorph '' tsupport w → Dw (Foundation.Parabolic.parabolicHomeomorph.symm y) i j = 0) ∧ (∀ (i j k : Fin 3), ∀ᵐ (y : Foundation.Parabolic.Vec3 × ℝ), y ∈ Ω ×ˢ I → y ∉ ⇑Foundation.Parabolic.parabolicHomeomorph '' tsupport w → D2w (Foundation.Parabolic.parabolicHomeomorph.symm y) i j k = 0) ∧ ∀ (i : Fin 3), ∀ᵐ (y : Foundation.Parabolic.Vec3 × ℝ), y ∈ Ω ×ˢ I → y ∉ ⇑Foundation.Parabolic.parabolicHomeomorph '' tsupport w → Dtw (Foundation.Parabolic.parabolicHomeomorph.symm y) i = 0

The first spatial, second spatial, and time weak derivatives vanish almost everywhere outside the closed support of a compactly supported field (lem:carleman-sobolev, ESS).