Time slicing and continuity of spatial integrals (for e.ergodic.break.up)

Source: enhance.tex 8305–8394. The joint spatial gradient of a function smooth up to t = 0 is continuous there, ‖∇θ‖²_{L²((0,1)×𝕋²)} is the iterated integral of the slice energies, and spatial integrals over the unit cube of jointly continuous integrands are continuous in time.

def AVenhance.Infra.Section5.LeftToShow.Slicing.closedCube : Set (Homogenization.Vec 2)

The closed unit square, a compact set carrying the open cube up to a null set.

Equations

• AVenhance.Infra.Section5.LeftToShow.Slicing.closedCube = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.LeftToShow.Slicing.isCompact_closedCube : IsCompact closedCube

theorem AVenhance.Infra.Section5.LeftToShow.Slicing.unitCube_subset_closedCube : unitCube ⊆ closedCube

theorem AVenhance.Infra.Section5.LeftToShow.Slicing.unitCube_ae_eq_closedCube : unitCube =ᵐ[MeasureTheory.volume] closedCube

theorem AVenhance.Infra.Section5.LeftToShow.continuous_vecNormSq_two : Continuous fun (v : Homogenization.Vec 2) => Homogenization.vecNormSq v

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

Continuous functions are integrable over the open unit cube.

theorem AVenhance.Infra.Section5.LeftToShow.fderiv_slice_eq_fderivWithin {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 ≤ t) (x v : Homogenization.Vec 2) : (fderiv ℝ (T t) x) v = (fderivWithin ℝ (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ) (t, x)) (0, v)

The slice derivative of a function smooth up to t = 0 is the within-derivative of the joint function in the spatial direction.

theorem AVenhance.Infra.Section5.LeftToShow.spaceGrad_continuousOn {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2) (Set.Ici 0 ×ˢ Set.univ)

The joint spatial gradient of a function smooth up to t = 0.

theorem AVenhance.Infra.Section5.LeftToShow.spaceTimeGradNormSq_eq_intervalIntegral {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hV : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2) (Set.Icc 0 1 ×ˢ Set.univ)) : spaceTimeGradNormSq V = ∫ (t : ℝ) in 0..1, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (V t x)

‖∇θ‖²_{L²((0,1)×𝕋²)} as an iterated integral of the slice energies.

theorem AVenhance.Infra.Section5.LeftToShow.continuousOn_integral_unitCube {h : ℝ → Homogenization.Vec 2 → ℝ} (hh : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => h p.1 p.2) (Set.Icc 0 1 ×ˢ Set.univ)) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, h t x) (Set.Icc 0 1)

Spatial integrals over the unit cube of jointly continuous integrands are continuous on [0,1].