Finite Fourier energy balance for a forced weak path

If every smooth periodic Fourier coefficient of a path satisfies an integral equation with integrable forcing, the finite Fourier projection satisfies the corresponding exact energy balance.

structure AVenhance.Infra.Section5.RelativeError.ForcedModePath (κ : ℝ) (f : Homogenization.Vec 2 → ℝ) (u : ℝ → Homogenization.Vec 2 → ℝ) (Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (G : ℝ × Homogenization.Vec 2 → ℝ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

The first seven regularity clauses of a weak solution together with the mode-path form of the forced weak equation ∂ₜu − κΔu = −G − div F, u(0) = f.

• slice_mem (t : ℝ) : t ∈ Set.Icc 0 1 → Homogenization.MemL2On unitCube (u t)
• memLp : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => u p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube)
• grad_memLp (i : Fin 2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Du p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)
• G_memLp : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict timeCube)
• F_memLp (i : Fin 2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => F p i) 2 (MeasureTheory.volume.restrict timeCube)
• weak_cont (ψ : Homogenization.Vec 2 → ℝ) : ContDiff ℝ (↑⊤) ψ → IsZ2Periodic ψ → ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, u t x * ψ x) (Set.Icc 0 1)
• path (ψ : Homogenization.Vec 2 → ℝ) : ContDiff ℝ (↑⊤) ψ → IsZ2Periodic ψ → ∀ t ∈ Set.Icc 0 1, ∫ (x : Homogenization.Vec 2) in unitCube, u t x * ψ x = (∫ (x : Homogenization.Vec 2) in unitCube, f x * ψ x) - ∫ (s : ℝ) in 0..t, forcedModeForcing κ Du G F ψ s

noncomputable def AVenhance.Infra.Section5.RelativeError.forcedMode (N : ℕ) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : Homogenization.Vec 2 → ℝ

The real Fourier mode with finite index i.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.forcedMode_smooth (N : ℕ) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : ContDiff ℝ (↑⊤) (forcedMode N i)

theorem AVenhance.Infra.Section5.RelativeError.forcedMode_periodic (N : ℕ) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : IsZ2Periodic (forcedMode N i)

theorem AVenhance.Infra.Section5.RelativeError.forced_finite_fourier_energy {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (h : ForcedModePath κ f u Du G F) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ‖Parabolic.WeakUniqueness.weakFourierCoefficientPath N u t‖ ^ 2 + ∫ (s : ℝ) in 0..t, 2 * ∑ i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N), Parabolic.WeakUniqueness.weakModePairing u (forcedMode N i) s * forcedModeForcing κ Du G F (forcedMode N i) s = ‖Parabolic.WeakUniqueness.weakFourierCoefficientPath N u 0‖ ^ 2

Coefficientwise energy balance for the finite Fourier projection of a forced path.