Strong spacetime cutoff convergence for weak solutions

This file turns the slice-wise Fourier cutoff estimates into the spacetime L² convergence needed to pass pairings in the finite weak energy identity.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_timeCube_measurable : MeasurableSet timeCube

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

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_Ioo_volume_lt_top : MeasureTheory.volume (Set.Ioo 0 1) < ⊤

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_finite_Ioo : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_timeCube_measure_eq_product : MeasureTheory.volume.restrict timeCube = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_finite_timeCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict timeCube)

def AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergyRegion (t : ℝ) : Set (ℝ × Homogenization.Vec 2)

Open time interval times the spatial unit cube for the weak energy integral.

Equations

• AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergyRegion t = Set.Ioo 0 t ×ˢ AVenhance.unitCube

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_region_measurable (t : ℝ) : MeasurableSet (weakEnergyRegion t)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_region_subset_timeCube {t : ℝ} (ht : t ∈ Set.Icc 0 1) : weakEnergyRegion t ⊆ timeCube

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_region_measure_eq_product (t : ℝ) : MeasureTheory.volume.restrict (weakEnergyRegion t) = (MeasureTheory.volume.restrict (Set.Ioo 0 t)).prod (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_region_weighted_integrable {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) {c : ℝ → ℝ} (hc : Continuous c) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => F p * c p.1) (MeasureTheory.volume.restrict (weakEnergyRegion t))

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_region_weighted_fubini {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) {c : ℝ → ℝ} (hc : Continuous c) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, F p * c p.1 = ∫ (s : ℝ) in Set.Ioo 0 t, c s * ∫ (x : Homogenization.Vec 2) in unitCube, F (s, x)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_Ioo_intervalIntegral {F : ℝ → ℝ} {t : ℝ} (ht : 0 ≤ t) : ∫ (s : ℝ) in Set.Ioo 0 t, F s = ∫ (s : ℝ) in 0..t, F s

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_region_integral_eq_interval {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, F p = ∫ (s : ℝ) in 0..t, ∫ (x : Homogenization.Vec 2) in unitCube, F (s, x)

Fubini on the truncated space-time cell, with the time variable written as an interval integral from the initial time.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_l2_pairing_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : |∫ (p : α), f p * g p ∂μ| ≤ √(∫ (p : α), f p ^ 2 ∂μ) * √(∫ (p : α), g p ^ 2 ∂μ)

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_drift_memLp_two {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) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (D p.1 p.2)) 2 (MeasureTheory.volume.restrict timeCube)

def AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyClamp (t : ℝ) : ℝ

Clamp an energy observation time to the closed unit interval.

Equations

• AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyClamp t = max 0 (min t 1)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyClamp_mem (t : ℝ) : weakEnergyClamp t ∈ Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyClamp_eq {t : ℝ} (ht : t ∈ Set.Icc 0 1) : weakEnergyClamp t = t

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyClamp_continuous : Continuous weakEnergyClamp

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyCoefficientExtension (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (i : Fin (FourierGalerkin.RealFourierDimension N)) (t : ℝ) : ℝ

Extend the weak solution's pairing with one real Fourier mode to all times.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyCoefficientExtension_continuous {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) (N : ℕ) (i : Fin (FourierGalerkin.RealFourierDimension N)) : Continuous (weakEnergyCoefficientExtension N u i)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyCoefficientExtension_eq (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (i : Fin (FourierGalerkin.RealFourierDimension N)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : weakEnergyCoefficientExtension N u i t = weakModePairing u (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) t

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyModeForcingIntegrand (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) (D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (N : ℕ) (i : Fin (FourierGalerkin.RealFourierDimension N)) (p : ℝ × Homogenization.Vec 2) : ℝ

Integrand for the forcing of a Fourier-mode pairing in the weak energy equation.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyModeForcingIntegrand_integrable {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) (N : ℕ) (i : Fin (FourierGalerkin.RealFourierDimension N)) : MeasureTheory.Integrable (weakEnergyModeForcingIntegrand b κ D N i) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyProjectionExpansion (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : weakFourierModeProjection N u t x = ∑ i : Fin (FourierGalerkin.RealFourierDimension N), weakModePairing u (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) t * FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i) x

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyProjectionGradientExpansion (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (j : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (weakFourierModeProjection N u t) x j = ∑ i : Fin (FourierGalerkin.RealFourierDimension N), weakModePairing u (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) t * spaceGrad (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) x j

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_modeForcingSum_eq (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) (D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (u : ℝ → Homogenization.Vec 2 → ℝ) (N : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : ∑ i : Fin (FourierGalerkin.RealFourierDimension N), weakModePairing u (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) t * weakEnergyModeForcingIntegrand b κ D N i (t, x) = Homogenization.vecDot (b t x) (D t x) * weakFourierModeProjection N u t x + κ * Homogenization.vecDot (D t x) (spaceGrad (weakFourierModeProjection N u t) x)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_singleMode_integral {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) (N : ℕ) (i : Fin (FourierGalerkin.RealFourierDimension N)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∫ (s : ℝ) in 0..t, weakModePairing u (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) s * weakModeForcing b κ D (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) s = ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, weakEnergyModeForcingIntegrand b κ D N i p * weakEnergyCoefficientExtension N u i p.1

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergy_finiteProjection_pairing_integral {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) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∫ (s : ℝ) in 0..t, 2 * ∑ i : Fin (FourierGalerkin.RealFourierDimension N), weakModePairing u (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) s * weakModeForcing b κ D (FourierGalerkin.realFourierModeAmbient N ((FourierGalerkin.realFourierIndexEquivFin N).symm i)) s = ∫ (p : ℝ × Homogenization.Vec 2) in weakEnergyRegion t, 2 * (Homogenization.vecDot (b p.1 p.2) (D p.1 p.2) * weakFourierModeProjection N u p.1 p.2 + κ * Homogenization.vecDot (D p.1 p.2) (spaceGrad (weakFourierModeProjection N u p.1) p.2))

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyProjectionExtension (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

Finite Fourier projection built from the extended weak mode pairings.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyProjectionExtension_continuous {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) (N : ℕ) : Continuous (weakEnergyProjectionExtension N u)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyProjectionExtension_eq_on (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (x : Homogenization.Vec 2) : weakEnergyProjectionExtension N u (t, x) = weakFourierModeProjection N u t x

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergyProjection_memLp {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) (N : ℕ) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => weakFourierModeProjection N u p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube)

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyGradientExtension (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (i : Fin 2) (p : ℝ × Homogenization.Vec 2) : ℝ

Coordinate gradient of the finite Fourier projection of a weak solution.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyGradientExtension_continuous {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) (N : ℕ) (i : Fin 2) : Continuous (weakEnergyGradientExtension N u i)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergyGradientExtension_eq_on (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (i : Fin 2) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (x : Homogenization.Vec 2) : weakEnergyGradientExtension N u i (t, x) = spaceGrad (weakFourierModeProjection N u t) x i

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEnergyGradient_memLp {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) (N : ℕ) (i : Fin 2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (weakFourierModeProjection N u p.1) p.2 i) 2 (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakEnergyPassage.weakEnergy_timeCube_integral_eq_Ioo_cell {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, F p = ∫ (t : ℝ) in Set.Ioo 0 1, ∫ (x : Homogenization.Vec 2) in unitCube, F (t, x)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjection_scalar_spacetime_L2_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) : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (u p.1 p.2 - weakFourierModeProjection N u p.1 p.2) ^ 2) Filter.atTop (nhds 0)

The finite real Fourier projections converge to a weak path in scalar spacetime L².

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakFourierProjection_gradient_spacetime_L2_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) : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (D p.1 p.2 i - spaceGrad (weakFourierModeProjection N u p.1) p.2 i) ^ 2) Filter.atTop (nhds 0)

Every weak-gradient coordinate is approximated by the corresponding projected derivative in spacetime L².