Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.Support.CarlemanCoreMixed

Commutation of space-time coordinate derivatives #

The commutator calculation in eq:carleman-commutator of the Escauriaza–Seregin–Šverák manuscript uses symmetry of the second derivative of a smooth scalar field.

source
theorem CKN.spatialPartial_eq_product_fderiv {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hf : DifferentiableAt ℝ f z) (i : Fin 3) :
spatialPartial f i z = (fderiv ℝ f z) (basisVec i, 0)

A spatial coordinate derivative is the ordinary space-time derivative in the corresponding coordinate direction.

source
theorem CKN.timePartial_eq_product_fderiv {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hf : DifferentiableAt ℝ f z) :
timePartial f z = (fderiv ℝ f z) (0, 1)

The time coordinate derivative is the ordinary space-time derivative in the time direction.

source
theorem CKN.spatialSecondPartial_comm {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) :
spatialSecondPartial f i j z = spatialSecondPartial f j i z

Smooth scalar fields have symmetric iterated spatial coordinate derivatives.

source
theorem CKN.timePartial_spatialPartial_comm {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (z : Foundation.Parabolic.Vec3 × ℝ) (i : Fin 3) :
timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial f i y) z = spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => timePartial f y) i z

Time and spatial coordinate differentiation commute for smooth scalar fields.

source
theorem CKN.spatialPartial_finsetSum_at {ι : Type u_1} (s : Finset ι) (f : ι → Foundation.Parabolic.Vec3 × ℝ → ℝ) {z : Foundation.Parabolic.Vec3 × ℝ} (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) z) (j : Fin 3) :
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => ∑ i ∈ s, f i y) j z = ∑ i ∈ s, spatialPartial (f i) j z

Spatial differentiation commutes with a finite sum of differentiable scalar fields.

source
theorem CKN.timePartial_finsetSum_at {ι : Type u_1} (s : Finset ι) (f : ι → Foundation.Parabolic.Vec3 × ℝ → ℝ) {z : Foundation.Parabolic.Vec3 × ℝ} (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) z) :
timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => ∑ i ∈ s, f i y) z = ∑ i ∈ s, timePartial (f i) z

Time differentiation commutes with a finite sum of differentiable scalar fields.

source
theorem CKN.spatialPartial_sub_at {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) (i : Fin 3) :
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => f y - g y) i z = spatialPartial f i z - spatialPartial g i z

A spatial coordinate derivative distributes over subtraction.

source
theorem CKN.timePartial_sub_at {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) :
timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => f y - g y) z = timePartial f z - timePartial g z

A time coordinate derivative distributes over subtraction.

source
theorem CKN.spatialPartial_add_at {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) (i : Fin 3) :
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => f y + g y) i z = spatialPartial f i z + spatialPartial g i z

A spatial coordinate derivative distributes over addition.

source
theorem CKN.timePartial_add_at {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {z : Foundation.Parabolic.Vec3 × ℝ} (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) :
timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => f y + g y) z = timePartial f z + timePartial g z

A time coordinate derivative distributes over addition.

source
@[instance_reducible]
def CKN.carlemanCoreMixedNormedAddCommGroup :
NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure used for mixed spatial derivatives.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable def CKN.carlemanCoreMixedNormedSpace :
    NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

    The real product normed-space structure used for mixed spatial derivatives.

    Equations
    Instances For
      source
      theorem CKN.spatialSecondPartial_comm_on {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i j : Fin 3) :
      spatialSecondPartial f i j z = spatialSecondPartial f j i z

      Coordinate second derivatives commute at every point where the phase is smooth on an open set.

      source
      theorem CKN.timePartial_spatialPartial_comm_on {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) (i : Fin 3) :
      timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial f i y) z = spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => timePartial f y) i z

      Time and spatial coordinate derivatives commute wherever the phase is smooth on an open set.