Discharge natural space-time integrability using the actual smooth scalar carrier and continuity of the conditional coefficient jets.

theorem AVenhance.Infra.Section4.iterate_timeCube_integrable_of_continuousOn {f : AmnrSpace → ℝ} (hf : ContinuousOn f (Set.Ici 0 ×ˢ Set.univ)) : MeasureTheory.IntegrableOn f timeCube MeasureTheory.volume

Continuous nonnegative-time fields are integrable on the time cell.

theorem AVenhance.Infra.Section4.iterate_word_gradient_smooth_up_to_initial {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => spaceGrad (iterateSpatialWord w (u z.1)) z.2) (Set.Ici 0 ×ˢ Set.univ)

Joint smoothness of every actual spatial word gradient, including time zero.

theorem AVenhance.Infra.Section4.iterate_word_gradient_energy_integrable {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (u z.1)) z.2)) timeCube MeasureTheory.volume

The actual smooth carrier supplies every word-gradient energy's integrability.

theorem AVenhance.Infra.Section4.iterateSplitFlux_continuousOn_of_jets (P : List (List (Fin 2) × List (Fin 2))) {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : ℝ → Homogenization.Vec 2 → ℝ} (hA : ∀ p ∈ P, ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) p.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (z : AmnrSpace) => iterateSplitFlux P (A z.1) (v z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)

The specified actual flux is continuous when its coefficient jets are continuous and its scalar has the smooth initial-time carrier.