Zero-data weak energy identity

The finite Fourier energy balances pass to the weak path using strong spacetime L² convergence of both the scalar and gradient cutoffs. The resulting identity is the input for uniqueness under a bounded drift.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakEnergy_unitCube_volume_lt_top : MeasureTheory.volume unitCube < ⊤

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.zeroData_memL2 : Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakEnergy_region_product_integrable {F G : ℝ × Homogenization.Vec 2 → ℝ} {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict timeCube)) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => F p * G p) (MeasureTheory.volume.restrict (weakEnergyRegion t))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakEnergy_square_integrable {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => F p ^ 2) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakEnergy_timeMarginal_intervalIntegrable {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) : IntervalIntegrable (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, F (s, x)) MeasureTheory.volume 0 1

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakEnergy_scalar_pairing_projection_tendsto {F U : ℝ × Homogenization.Vec 2 → ℝ} {t : ℝ} (ht : t ∈ Set.Icc 0 1) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict timeCube)) (hU : MeasureTheory.MemLp U 2 (MeasureTheory.volume.restrict timeCube)) (P : ℕ → ℝ × Homogenization.Vec 2 → ℝ) (he : ∀ (N : ℕ), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => U p - P N p) 2 (MeasureTheory.volume.restrict timeCube)) (henergy : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (U p - P N p) ^ 2) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, F p * P N p) Filter.atTop (nhds (∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, F p * U p))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakEnergy_driftPairing_projection_tendsto {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) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, Homogenization.vecDot (b p.1 p.2) (D p.1 p.2) * weakFourierModeProjection N u p.1 p.2) Filter.atTop (nhds (∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, Homogenization.vecDot (b p.1 p.2) (D p.1 p.2) * u p.1 p.2))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakEnergy_gradientPairing_projection_tendsto {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) (i : Fin 2) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, D p.1 p.2 i * spaceGrad (weakFourierModeProjection N u p.1) p.2 i) Filter.atTop (nhds (∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, D p.1 p.2 i ^ 2))

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

A weak solution satisfies the full weak energy identity at every time. The drift term is kept signed; boundedness of the drift is used only to justify the spacetime L² pairing passage.

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

The zero-datum energy identity is the corresponding specialization of the full identity.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_zero_data_energy_inequality {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ (fun (x : Homogenization.Vec 2) => 0) 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) (hκ : 0 < κ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ t ∈ Set.Icc 0 1, l2NormSq (u t) ≤ B ^ 2 / κ * ∫ (s : ℝ) in 0..t, l2NormSq (u s)

The zero-data energy identity and the pointwise drift bound imply the parabolic energy inequality, with the diffusion term absorbed by Young's inequality.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_zero_data_l2NormSq_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ (fun (x : Homogenization.Vec 2) => 0) 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) : ContinuousOn (fun (t : ℝ) => l2NormSq (u t)) (Set.Icc 0 1)

The exact weak energy identity makes the squared L² norm path continuous on the closed time interval. The weak-test continuity in the class is the endpoint input to the Fourier energy identity.

def AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakZeroEnergyClamp (t : ℝ) : ℝ

Clamp time to the closed unit interval in the zero-initial-data energy argument.

Equations

• AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakZeroEnergyClamp t = max 0 (min t 1)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakZeroEnergyClamp_mem (t : ℝ) : weakZeroEnergyClamp t ∈ Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakZeroEnergyClamp_eq {t : ℝ} (ht : t ∈ Set.Icc 0 1) : weakZeroEnergyClamp t = t

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ZeroDataEnergy.weakZeroEnergyClamp_continuous : Continuous weakZeroEnergyClamp

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_zero_data_eq_zero {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsWeakSolutionGrad b κ (fun (x : Homogenization.Vec 2) => 0) 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) (hκ : 0 < κ) (t : ℝ) : t ∈ Set.Icc 0 1 → l2NormSq (u t) = 0

A bounded drift cannot support a nonzero zero-data weak solution.