Divergence-free weak energy identities for §5

The endpoint energy input follows from the weak energy identity for L² data. The well-posedness input is discharged by the weak well-posedness proof.

theorem AVenhance.Infra.Section5.weak_solution_divFree_difference_energy_identity (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {κ : ℝ} {f g : Homogenization.Vec 2 → ℝ} {θ η : ℝ → Homogenization.Vec 2 → ℝ} {Dθ Dη : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) (hθ : IsWeakSolutionGrad b κ f θ Dθ) (hη : IsWeakSolutionGrad b κ g η Dη) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) (hdiv : IsDivFree b) : (l2NormSq (θ 1 - η 1) + 2 * κ * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => Dθ t x - Dη t x) = l2NormSq (f - g)

Difference energy identity in the source class used by the §5 reduction.

theorem AVenhance.Infra.Section5.differenceEnergyInput_of_divFree_and_l2Data (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) (hdiv : IsDivFree b) : DifferenceEnergyInput b

§5 DifferenceEnergyInput, with the L² data hypotheses used by every reduction consumer.

theorem AVenhance.Infra.Section5.weakWellposedInput_of_A1 (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) : WeakWellposedInput b

The weak well-posedness theorem supplies the existence-and-uniqueness input used by the H¹ reduction.

theorem AVenhance.Infra.Section5.divFree_energy_dissipation_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ f u D) (hf : Homogenization.MemL2On unitCube f) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t)) (hdiv : IsDivFree b) : κ * spaceTimeGradNormSq D ≤ l2NormSq f / 2

A weak solution with divergence-free periodic drift satisfies the exact energy input used by the conditional §5.4 dissipation bound.