Time sections of space-time weak derivatives

This module extracts the one-dimensional weak time derivative on almost every spatial section from the space-time identity in def:sws.

def ESS.timeCompact (τ : ℝ) (n : ℕ) : Set ℝ

The compact inner interval used to exhaust the positive time interval (0, τ).

Equations

• ESS.timeCompact τ n = Set.Icc (τ / (↑n + 2)) (τ - τ / (↑n + 2))

structure ESS.IntervalTestWithSupport (τ : ℝ) (n : ℕ) : Type

A smooth compactly supported time test whose support lies in one inner interval.

• toFun : ℝ → ℝ

  The scalar time test.

• smooth : ContDiff ℝ (↑⊤) self.toFun
• compact : HasCompactSupport self.toFun
• supportInterval : tsupport self.toFun ⊆ Set.Ioo 0 τ
• supportCompact : tsupport self.toFun ⊆ timeCompact τ n

noncomputable def ESS.intervalTestPair {τ : ℝ} {n : ℕ} (φ : IntervalTestWithSupport τ n) : C(ℝ, ℝ) × C(ℝ, ℝ)

A time test and its first derivative, viewed as a pair of continuous functions.

Equations

• ESS.intervalTestPair φ = ({ toFun := φ.toFun, continuous_toFun := ⋯ }, { toFun := deriv φ.toFun, continuous_toFun := ⋯ })

noncomputable def ESS.sectionTimePairing {τ : ℝ} (w Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (i : Fin 3) (ψ : ℝ → ℝ) (x : CKN.Foundation.Parabolic.Vec3) : ℝ

The weak time derivative pairing on the spatial section at x.

Equations

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

theorem ESS.hasSectionwiseTimeWeakDeriv_of_hasSpaceTimeWeakDerivs {B : Set CKN.Foundation.Parabolic.Vec3} {τ : ℝ} (hB : IsOpen B) (hτ : 0 < τ) {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hwcont : ContinuousOn w (CKN.spaceTimeSet B (Set.Ico 0 τ))) (hDtwL2 : MeasureTheory.MemLp Dtw 2 ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ)))) (hderiv : CKN.HasSpaceTimeWeakDerivs B (Set.Ioo 0 τ) w Dw D2w Dtw) : ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ∀ (i : Fin 3), CKN.HasWeakDerivOn (Set.Ioo 0 τ) (fun (s : ℝ) => w (have this := (x, s); this) i) fun (s : ℝ) => Dtw (have this := (x, s); this) i

The time clause of the space-time weak derivative identity holds on almost every spatial section, as required in lem:ftc-small-time.