Time differentiation of the periodic quadratic energy.

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

Joint time-space domain with strictly positive time.

Equations

• AVenhance.Infra.Section4.classicalPositiveTimeDomain = AVenhance.Infra.Classical.classicalPositiveTimeDomain

theorem AVenhance.Infra.Section4.ThetaTimeEnergy.thetaTime_unitCube_subset_closedCell : unitCube ⊆ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

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

theorem AVenhance.Infra.Section4.thetaTime_integrableOn_unitCube {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

theorem AVenhance.Infra.Section4.thetaTime_measurableSet_unitCube : MeasurableSet unitCube

def AVenhance.Infra.Section4.ThetaTimeEnergy.timeVector : ℝ × Homogenization.Vec 2

Pure time direction in the temperature energy calculation.

Equations

• AVenhance.Infra.Section4.ThetaTimeEnergy.timeVector = AVenhance.Infra.Classical.TimeEnergy.timeVector

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

Time partial derivative obtained from the joint Fréchet derivative of the temperature.

Equations

• AVenhance.Infra.Section4.classicalTimePartial u p = AVenhance.Infra.Classical.classicalTimePartial u p

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

theorem AVenhance.Infra.Section4.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.Section4.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.Section4.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.Section4.classicalSmooth_slice {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (u t)

theorem AVenhance.Infra.Section4.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.Section4.classicalContinuous_slice {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) classicalPositiveTimeDomain) {t : ℝ} (ht : 0 < t) : Continuous (u t)

theorem AVenhance.Infra.Section4.theta_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 unitCube, u s x ^ 2) (∫ (x : Homogenization.Vec 2) in unitCube, 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.Section4.theta_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 unitCube, 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.