Shared positive-time calculus and differentiation of periodic quadratic energy.

def AVenhance.Infra.Classical.classicalPositiveTimeDomain : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with strictly positive time.

Equations

• AVenhance.Infra.Classical.classicalPositiveTimeDomain = Set.Ioi 0 ×ˢ Set.univ

theorem AVenhance.Infra.Classical.TimeEnergy.unitCell_subset_closedUnitCell : Torus.unitCell 2 ⊆ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Classical.TimeEnergy.isCompact_closedUnitCell : IsCompact (Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1)

theorem AVenhance.Infra.Classical.continuous_integrableOn_unitCell {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

def AVenhance.Infra.Classical.TimeEnergy.timeVector : ℝ × Homogenization.Vec 2

Pure time direction in the joint time-space domain.

Equations

• AVenhance.Infra.Classical.TimeEnergy.timeVector = (1, 0)

noncomputable def AVenhance.Infra.Classical.classicalTimePartial (u : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

Time partial derivative obtained by evaluating the joint Fréchet derivative.

Equations

• AVenhance.Infra.Classical.classicalTimePartial u p = (fderiv ℝ (Function.uncurry u) p) AVenhance.Infra.Classical.TimeEnergy.timeVector

theorem AVenhance.Infra.Classical.TimeEnergy.partialTime_continuousOn {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) : ContinuousOn (classicalTimePartial u) classicalPositiveTimeDomain

theorem AVenhance.Infra.Classical.classicalTimeSection_hasDerivAt {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasDerivAt (fun (s : ℝ) => u s x) (classicalTimePartial u (t, x)) t

theorem AVenhance.Infra.Classical.classicalTimePartial_eq_deriv {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : classicalTimePartial u (t, x) = deriv (fun (s : ℝ) => u s x) t

The joint smooth representative's time partial is the ordinary derivative of a fixed spatial section at every positive time.

theorem AVenhance.Infra.Classical.classicalTimePartial_continuous_slice {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) : Continuous fun (x : Homogenization.Vec 2) => classicalTimePartial u (t, x)

theorem AVenhance.Infra.Classical.classicalSmooth_slice {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (u t)

theorem AVenhance.Infra.Classical.classicalSmooth_slice_nonneg {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (u t)

theorem AVenhance.Infra.Classical.classicalContinuous_slice {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) : Continuous (u t)

theorem AVenhance.Infra.Classical.unitCell_energy_hasDerivAt {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u s x ^ 2) (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, 2 * u t x * classicalTimePartial u (t, x)) t

The unit-cell quadratic energy is differentiable at every positive time, with the expected pointwise time derivative under the integral.

theorem AVenhance.Infra.Classical.unitCell_energy_continuousOn {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) {T : ℝ} (hT : 0 ≤ T) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u t x ^ 2) (Set.Icc 0 T)

The cell energy is continuous down to the initial time for a jointly smooth function on the closed nonnegative time half-space.