The difference of two weak solutions as a forced path #
If θ and θ_M are weak solutions with the same datum and diffusivity but different
drifts, the difference w = θ - θ_M satisfies the forced mode-path equation for the drift of
θ, with transport density b·Dw and any flux F representing (b - b_M)·Dθ_M against smooth
periodic tests.
theorem
AVenhance.Infra.Section5.RelativeError.weak_modeDensity_integrable
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{g : Homogenization.Vec 2 → ℝ}
{θ : ℝ → Homogenization.Vec 2 → ℝ}
{Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hθ : IsWeakSolutionGrad b κ g θ Dθ)
{ψ : Homogenization.Vec 2 → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
:
MeasureTheory.Integrable
(fun (p : ℝ × Homogenization.Vec 2) =>
Homogenization.vecDot (b p.1 p.2) (Dθ p.1 p.2) * ψ p.2 + κ * Homogenization.vecDot (Dθ p.1 p.2) (spaceGrad ψ p.2))
(MeasureTheory.volume.restrict timeCube)
Pairing of a weak solution's mode density with a smooth periodic mode is integrable on the time cell.
theorem
AVenhance.Infra.Section5.RelativeError.difference_forcedModePath
{b bM : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{g : Homogenization.Vec 2 → ℝ}
{θ θM : ℝ → Homogenization.Vec 2 → ℝ}
{Dθ DM : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hθ : IsWeakSolutionGrad b κ g θ Dθ)
(hM : IsWeakSolutionGrad bM κ g θM DM)
(hg : Homogenization.MemL2On unitCube g)
(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)
{F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2}
(hF :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => F p i) 2 (MeasureTheory.volume.restrict timeCube))
(hflux :
∀ s ∈ Set.Icc 0 1,
∀ (ψ : Homogenization.Vec 2 → ℝ),
ContDiff ℝ (↑⊤) ψ →
IsZ2Periodic ψ →
MeasureTheory.Integrable
(fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b s x - bM s x) (DM s x) * ψ x)
(MeasureTheory.volume.restrict unitCube) ∧ ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (b s x - bM s x) (DM s x) * ψ x = ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (F (s, x)) (spaceGrad ψ x))
:
ForcedModePath κ (fun (x : Homogenization.Vec 2) => 0) (fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x)
(fun (t : ℝ) (x : Homogenization.Vec 2) => Dθ t x - DM t x)
(fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (Dθ p.1 p.2 - DM p.1 p.2)) F
The difference of two weak solutions with the same datum and diffusivity satisfies the
forced mode-path equation, provided the cross transport (b - b_M)·Dθ_M is represented by the
flux F against every smooth periodic mode.
theorem
AVenhance.Infra.Section5.RelativeError.tendsto_integral_sq_sub
{μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)}
{a c : ℕ → ℝ × Homogenization.Vec 2 → ℝ}
(ha : ∀ (N : ℕ), MeasureTheory.MemLp (a N) 2 μ)
(hc : ∀ (N : ℕ), MeasureTheory.MemLp (c N) 2 μ)
(h1 : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2), a N p ^ 2 ∂μ) Filter.atTop (nhds 0))
(h2 : Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2), c N p ^ 2 ∂μ) Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (N : ℕ) => ∫ (p : ℝ × Homogenization.Vec 2), (a N p - c N p) ^ 2 ∂μ) Filter.atTop (nhds 0)
Squeeze for the square of a difference of two L²-null sequences.
theorem
AVenhance.Infra.Section5.RelativeError.weakModePairing_sub
{θ θM : ℝ → Homogenization.Vec 2 → ℝ}
{ψ : Homogenization.Vec 2 → ℝ}
{t : ℝ}
(hθ : Homogenization.MemL2On unitCube (θ t))
(hM : Homogenization.MemL2On unitCube (θM t))
(hψ : Homogenization.MemL2On unitCube ψ)
:
Parabolic.WeakUniqueness.weakModePairing (fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x) ψ t = Parabolic.WeakUniqueness.weakModePairing θ ψ t - Parabolic.WeakUniqueness.weakModePairing θM ψ t
The Fourier coefficients of a difference are the differences of the coefficients.
theorem
AVenhance.Infra.Section5.RelativeError.projection_sub_apply
{θ θM : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(N : ℕ)
(hθ : Homogenization.MemL2On unitCube (θ t))
(hM : Homogenization.MemL2On unitCube (θM t))
(x : Homogenization.Vec 2)
:
Parabolic.WeakUniqueness.weakFourierModeProjection N (fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x) t x = Parabolic.WeakUniqueness.weakFourierModeProjection N θ t x - Parabolic.WeakUniqueness.weakFourierModeProjection N θM t x
theorem
AVenhance.Infra.Section5.RelativeError.projection_grad_sub_apply
{θ θM : ℝ → Homogenization.Vec 2 → ℝ}
{t : ℝ}
(N : ℕ)
(hθ : Homogenization.MemL2On unitCube (θ t))
(hM : Homogenization.MemL2On unitCube (θM t))
(x : Homogenization.Vec 2)
(j : Fin 2)
:
spaceGrad
(Parabolic.WeakUniqueness.weakFourierModeProjection N (fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x) t)
x j = spaceGrad (Parabolic.WeakUniqueness.weakFourierModeProjection N θ t) x j - spaceGrad (Parabolic.WeakUniqueness.weakFourierModeProjection N θM t) x j
theorem
AVenhance.Infra.Section5.RelativeError.difference_projection_tendsto
{b bM : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{g : Homogenization.Vec 2 → ℝ}
{θ θM : ℝ → Homogenization.Vec 2 → ℝ}
{Dθ DM : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hθ : IsWeakSolutionGrad b κ g θ Dθ)
(hM : IsWeakSolutionGrad bM κ g θM DM)
:
Filter.Tendsto
(fun (N : ℕ) =>
∫ (p : ℝ × Homogenization.Vec 2) in timeCube, (θ p.1 p.2 - θM p.1 p.2 - Parabolic.WeakUniqueness.weakFourierModeProjection N
(fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x) p.1 p.2) ^ 2)
Filter.atTop (nhds 0) ∧ ∀ (i : Fin 2),
Filter.Tendsto
(fun (N : ℕ) =>
∫ (p : ℝ × Homogenization.Vec 2) in timeCube, ((Dθ p.1 p.2 - DM p.1 p.2) i - spaceGrad
(Parabolic.WeakUniqueness.weakFourierModeProjection N
(fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - θM t x) p.1)
p.2 i) ^ 2)
Filter.atTop (nhds 0)
Spacetime L² convergence of the Fourier projections of a difference of weak solutions.