Static divergence-free cancellation on periodic H¹

For a bounded measurable periodic field that is divergence free against smooth periodic tests, the transport pairing ∫ b·Du u vanishes for every periodic H¹ function u. The public names below reuse the Fourier approximation argument of Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.

theorem AVenhance.Infra.Section5.RelativeError.divFreeEnergyFiniteUnitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.RelativeError.divFreeEnergyFiniteUnitCell : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Torus.unitCell 2))

@[instance_reducible]

noncomputable def AVenhance.Infra.Section5.RelativeError.divFreeEnergyMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• AVenhance.Infra.Section5.RelativeError.divFreeEnergyMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem AVenhance.Infra.Section5.RelativeError.divFreeEnergyIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Section5.RelativeError.divFreeEnergyProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.divFreeEnergyProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyStatic.divFree_torusInner_cell {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : inner ℝ (MeasureTheory.MemLp.toLp (Torus.periodicToTorus f) ⋯) (MeasureTheory.MemLp.toLp (Torus.periodicToTorus g) ⋯) = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * g x

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyStatic.divFree_unitCube_measurable : MeasurableSet unitCube

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyStatic.divFree_component_memLp_top_cell {b : Homogenization.Vec 2 → Homogenization.Vec 2} (hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C) (i : Fin 2) : MeasureTheory.MemLp (fun (x : Homogenization.Vec 2) => b x i) ⊤ (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyStatic.divFree_periodicComponent_memLp_top_torus {b : Homogenization.Vec 2 → Homogenization.Vec 2} (hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C) (i : Fin 2) : MeasureTheory.MemLp (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => b x i) ⊤ MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyStatic.divFree_torus_product_memLp_two {b : Homogenization.Vec 2 → Homogenization.Vec 2} (hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C) {g : Homogenization.Vec 2 → ℝ} (hg : Homogenization.MemL2On unitCube g) (i : Fin 2) : MeasureTheory.MemLp (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => b x i * g x) 2 MeasureTheory.volume

theorem AVenhance.Infra.Section5.RelativeError.ForcedEnergyStatic.divFree_cell_pairing_tendsto {F : ℕ → Homogenization.Vec 2 → ℝ} {f g : Homogenization.Vec 2 → ℝ} (hFN : ∀ (N : ℕ), Homogenization.MemL2On unitCube (F N)) (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) (hconv : Filter.Tendsto (fun (N : ℕ) => MeasureTheory.MemLp.toLp (Torus.periodicToTorus (F N)) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp (Torus.periodicToTorus f) ⋯))) : Filter.Tendsto (fun (N : ℕ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, F N x * g x) Filter.atTop (nhds (∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * g x))

theorem AVenhance.Infra.Section5.RelativeError.static_divFree_h1_cancellation {b : Homogenization.Vec 2 → Homogenization.Vec 2} (hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C) (hdiv : ∀ (f : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) f → IsZ2Periodic f → ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (b x) (spaceGrad f x) = 0) {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsPeriodicH1With u Du) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (b x) (Du x) * u x = 0