Time derivative of the periodic energy of a jointly C¹ function

The classical TimeEnergy development assumes the joint function is C^∞. The forced energy estimate applies it to w = u - v, where v is only jointly C²; here the same statements are proved from joint C¹ regularity on [0,∞) × ℝ².

theorem AVenhance.Infra.Section5.Integration.Energy.isOpen_positiveTimeDomain : IsOpen Classical.classicalPositiveTimeDomain

def AVenhance.Infra.Section5.Integration.Energy.TimeDerivative.closedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section5.Integration.Energy.TimeDerivative.closedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.Integration.Energy.TimeDerivative.isCompact_closedCell : IsCompact closedCell

theorem AVenhance.Infra.Section5.Integration.Energy.TimeDerivative.unitCell_subset_closedCell : Torus.unitCell 2 ⊆ closedCell

theorem AVenhance.Infra.Section5.Integration.Energy.timeSection_hasDerivAt_one {g : ℝ → Homogenization.Vec 2 → ℝ} (hg : ContDiffOn ℝ 1 (Function.uncurry g) Classical.classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasDerivAt (fun (s : ℝ) => g s x) ((fderiv ℝ (Function.uncurry g) (t, x)) (1, 0)) t

The time derivative of a fixed spatial section, read from the joint Fréchet derivative.

theorem AVenhance.Infra.Section5.Integration.Energy.deriv_timeSection_eq {g : ℝ → Homogenization.Vec 2 → ℝ} (hg : ContDiffOn ℝ 1 (Function.uncurry g) Classical.classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : deriv (fun (s : ℝ) => g s x) t = (fderiv ℝ (Function.uncurry g) (t, x)) (1, 0)

theorem AVenhance.Infra.Section5.Integration.Energy.continuousOn_timePartial_one {g : ℝ → Homogenization.Vec 2 → ℝ} (hg : ContDiffOn ℝ 1 (Function.uncurry g) Classical.classicalPositiveTimeDomain) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => (fderiv ℝ (Function.uncurry g) p) (1, 0)) Classical.classicalPositiveTimeDomain

theorem AVenhance.Infra.Section5.Integration.Energy.continuous_slice_one {g : ℝ → Homogenization.Vec 2 → ℝ} (hg : ContDiffOn ℝ 1 (Function.uncurry g) Classical.classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) : Continuous (g t)

theorem AVenhance.Infra.Section5.Integration.Energy.continuous_timePartial_slice_one {g : ℝ → Homogenization.Vec 2 → ℝ} (hg : ContDiffOn ℝ 1 (Function.uncurry g) Classical.classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) : Continuous fun (x : Homogenization.Vec 2) => (fderiv ℝ (Function.uncurry g) (t, x)) (1, 0)

theorem AVenhance.Infra.Section5.Integration.Energy.energy_hasDerivAt_one {g : ℝ → Homogenization.Vec 2 → ℝ} (hg : ContDiffOn ℝ 1 (Function.uncurry g) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, g s x ^ 2) (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, 2 * g t x * deriv (fun (s : ℝ) => g s x) t) t

The unit-cell quadratic energy of a jointly C¹ function is differentiable at positive times.