Integral paths for weak Fourier coefficients

Testing the weak equation by a spatial Fourier mode and a smooth time factor gives an ordinary scalar weak equation. The scalar reconstruction lemma then identifies each coefficient with its absolutely continuous forcing path.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ModePath.modePath_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.ModePath.modePath_timeMeasure_Ioo_eq_Ioc : MeasureTheory.volume.restrict (Set.Ioo 0 1) = MeasureTheory.volume.restrict (Set.Ioc 0 1)

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

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

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakModePairing (u : ℝ → Homogenization.Vec 2 → ℝ) (ψ : Homogenization.Vec 2 → ℝ) (t : ℝ) : ℝ

Cell pairing with one smooth periodic spatial test.

Equations

• AVenhance.Infra.Parabolic.WeakUniqueness.weakModePairing u ψ t = ∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, u t x * ψ x

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakModeForcing (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) (D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (ψ : Homogenization.Vec 2 → ℝ) (t : ℝ) : ℝ

The scalar forcing seen by a smooth spatial weak test.

Equations

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ModePath.modePath_timeCube_measurable : MeasurableSet timeCube

theorem AVenhance.Infra.Parabolic.WeakUniqueness.ModePath.modePath_continuous_joint_bound {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : Continuous F) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᵐ (p : ℝ × Homogenization.Vec 2) ∂MeasureTheory.volume.restrict timeCube, ‖F p‖ ≤ C

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_mode_integral_path {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) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψper : IsZ2Periodic ψ) (t : ℝ) : t ∈ Set.Icc 0 1 → weakModePairing u ψ t = weakModePairing (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => f x_1) ψ 0 - ∫ (s : ℝ) in 0..t, weakModeForcing b κ D ψ s

Every fixed smooth periodic Fourier coefficient of a weak solution satisfies its integral equation on the whole closed time interval.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_solution_mode_forcing_intervalIntegrable {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) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : IntervalIntegrable (weakModeForcing b κ D ψ) MeasureTheory.volume 0 1

The scalar forcing paired with a smooth periodic mode is integrable on the full time interval. This is the coefficientwise input for the finite-dimensional energy balance.