Divergence-free transport cancellation and the weak energy identity

The compact cutoff from Infra.Heat.PeriodicCutoff turns distributional divergence-free tests on the plane into periodic tests on the torus. Fourier approximation then extends the cancellation to the periodic H¹ carrier.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.divFreeEnergyFiniteUnitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.divFreeEnergyFiniteUnitCell : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Torus.unitCell 2))

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.divFreeEnergyMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.divFreeEnergyIsAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Parabolic.WeakUniqueness.divFreeEnergyProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.WeakUniqueness.divFreeEnergyProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFreeClosedBox : Set (Homogenization.Vec 2)

Closed symmetric unit box used for the divergence-free energy cutoff.

Equations

• AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFreeClosedBox = Set.univ.pi fun (x : Fin 2) => Set.Icc (-1) 1

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFreeClosedBox_compact : IsCompact divFreeClosedBox

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFreeTile_subset_closedBox (b : Bool × Bool) : Heat.heatPeriodicTile b ⊆ divFreeClosedBox

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFree_continuous_bound_on_box {F : Homogenization.Vec 2 → ℝ} (hF : Continuous F) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ x ∈ divFreeClosedBox, ‖F x‖ ≤ M

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFree_tile_volume_lt_top (b : Bool × Bool) : MeasureTheory.volume (Heat.heatPeriodicTile b) < ⊤

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFree_component_factor_integrable_on {b : Homogenization.Vec 2 → Homogenization.Vec 2} (hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C) {F : Homogenization.Vec 2 → ℝ} (hF : Continuous F) (hFBound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ x ∈ divFreeClosedBox, ‖F x‖ ≤ M) {S : Set (Homogenization.Vec 2)} (hS : S ⊆ divFreeClosedBox) (hSmeas : MeasurableSet S) (hSfinite : MeasureTheory.volume S < ⊤) (i : Fin 2) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => b x i * F x) S MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFree_component_factor_integrable_tile {b : Homogenization.Vec 2 → Homogenization.Vec 2} (hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C) {F : Homogenization.Vec 2 → ℝ} (hF : Continuous F) (hFBound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ x ∈ divFreeClosedBox, ‖F x‖ ≤ M) (i : Fin 2) (tile : Bool × Bool) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => b x i * F x) (Heat.heatPeriodicTile tile) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.frozenPeriodic_to_heatPeriodic {F : Homogenization.Vec 2 → ℝ} (hF : IsZ2Periodic F) : Torus.IsZdPeriodic F

theorem AVenhance.Infra.Parabolic.WeakUniqueness.isDivFree_integral_periodic_smooth_test {b : Homogenization.Vec 2 → Homogenization.Vec 2} (hbMeas : MeasureTheory.AEStronglyMeasurable b MeasureTheory.volume) (hbBound : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖b x‖ ≤ C) (hbPeriodic : IsZ2Periodic b) (hDiv : ∀ (φ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → ∫ (x : Homogenization.Vec 2), Homogenization.vecDot (b x) (spaceGrad φ x) = 0) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfPeriodic : IsZ2Periodic f) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (b x) (spaceGrad f x) = 0

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.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.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFree_unitCube_measurable : MeasurableSet unitCube

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.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.Parabolic.WeakUniqueness.DivergenceFreeEnergy.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.Parabolic.WeakUniqueness.DivergenceFreeEnergy.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.Parabolic.WeakUniqueness.DivergenceFreeEnergy.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.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFree_static_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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.DivergenceFreeEnergy.divFree_openCylinder_measure : MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.univ) = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_divFree_drift_pairing_zero {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) (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) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, Homogenization.vecDot (b p.1 p.2) (D p.1 p.2) * u p.1 p.2 = 0

For a divergence-free periodic drift, the signed transport contribution in the weak energy identity vanishes on every truncated time-space cell. The slice cancellation holds a.e. in time, which is all the Fubini representation of the spacetime integral requires.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_divFree_energy_identity {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) (t : ℝ) : t ∈ Set.Icc 0 1 → l2NormSq (u t) + 2 * κ * ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 t ×ˢ unitCube, Homogenization.vecNormSq (D p.1 p.2) = l2NormSq f

The signed weak energy identity reduces to the exact divergence-free energy identity on the periodic class.