Forced Fourier mode calculus on the space-time cell

Support lemmas for the forced weak energy identity: the forcing seen by a smooth periodic spatial mode, its integrability, and the finite Fourier sums attached to a weak path.

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

noncomputable def AVenhance.Infra.Section5.RelativeError.forcedModeIntegrand (κ : ℝ) (Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (G : ℝ × Homogenization.Vec 2 → ℝ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (ψ : Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

The forcing density seen by a smooth spatial mode ψ: transport/forcing scalar G, diffusion κ Du·∇ψ and flux F·∇ψ.

Equations

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

noncomputable def AVenhance.Infra.Section5.RelativeError.forcedModeForcing (κ : ℝ) (Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (G : ℝ × Homogenization.Vec 2 → ℝ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (ψ : Homogenization.Vec 2 → ℝ) (s : ℝ) : ℝ

The time-slice integral of forcedModeIntegrand.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.forced_timeCube_measure_eq_product : MeasureTheory.volume.restrict timeCube = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.RelativeError.forced_timeCube_measurable : MeasurableSet timeCube

theorem AVenhance.Infra.Section5.RelativeError.forcedFiniteTimeCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Section5.RelativeError.forced_continuous_bound {Z : Homogenization.Vec 2 → ℝ} (hZ : Continuous Z) : ∃ (C : ℝ), ∀ᵐ (p : ℝ × Homogenization.Vec 2) ∂MeasureTheory.volume.restrict timeCube, ‖Z p.2‖ ≤ C

A continuous bounded function of the spatial variable alone is bounded on the time cell.

theorem AVenhance.Infra.Section5.RelativeError.forced_vecDot_integrable {Y : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hY : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Y p i) 2 (MeasureTheory.volume.restrict timeCube)) {Z : Homogenization.Vec 2 → Homogenization.Vec 2} (hZ : Continuous Z) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (Y p) (Z p.2)) (MeasureTheory.volume.restrict timeCube)

A coordinatewise L² field paired with a continuous spatial field is integrable.

theorem AVenhance.Infra.Section5.RelativeError.forcedModeIntegrand_integrable {κ : ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hDu : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Du p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict timeCube)) (hF : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => F p i) 2 (MeasureTheory.volume.restrict timeCube)) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : MeasureTheory.Integrable (forcedModeIntegrand κ Du G F ψ) (MeasureTheory.volume.restrict timeCube)

The mode forcing density is integrable on the time cell.

theorem AVenhance.Infra.Section5.RelativeError.forcedModeForcing_intervalIntegrable {κ : ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hDu : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Du p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict timeCube)) (hF : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => F p i) 2 (MeasureTheory.volume.restrict timeCube)) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : IntervalIntegrable (forcedModeForcing κ Du G F ψ) MeasureTheory.volume 0 1

Mode forcing is interval integrable on [0,1].