The limit profile of a uniformly L²-Cauchy family of space-time functions #
Given θ j : ℝ → Vec 2 → ℝ that are slice-wise and jointly L² and uniformly Cauchy in
L²(cell) over t ∈ [0,1], a fast subsequence defines an everywhere-defined limit Θ (via
limUnder) which is periodic, slice-wise and jointly L², and is the uniform L² limit.
theorem
AVenhance.Infra.FullTheorem.TransportLimit.joint_eLpNorm_le
{F : ℝ × Homogenization.Vec 2 → ℝ}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict timeCube))
{η : ℝ}
(hη : 0 ≤ η)
(h : ∀ t ∈ Set.Ioo 0 1, √(∫ (x : Homogenization.Vec 2) in unitCube, F (t, x) ^ 2) ≤ η)
:
Fubini bound on the space-time cell from slice bounds.
noncomputable def
AVenhance.Infra.FullTheorem.TransportLimit.limitProfile
(θ : ℕ → ℝ → Homogenization.Vec 2 → ℝ)
(s : ℕ → ℕ)
(t : ℝ)
(x : Homogenization.Vec 2)
:
The limit profile along the subsequence s.
Equations
- AVenhance.Infra.FullTheorem.TransportLimit.limitProfile θ s t x = Filter.atTop.limUnder fun (k : ℕ) => θ (s k) t x
Instances For
theorem
AVenhance.Infra.FullTheorem.TransportLimit.limitProfile_periodic
{θ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{s : ℕ → ℕ}
{t : ℝ}
(hper : ∀ (j : ℕ), IsZ2Periodic (θ j t))
:
IsZ2Periodic (limitProfile θ s t)
theorem
AVenhance.Infra.FullTheorem.TransportLimit.exists_uniform_l2_limit
(θ : ℕ → ℝ → Homogenization.Vec 2 → ℝ)
(hper : ∀ (j : ℕ), ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (θ j t))
(hmem : ∀ (j : ℕ), ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (θ j t))
(hjoint :
∀ (j : ℕ),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => θ j p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube))
(hcau :
∀ (η : ℝ),
0 < η →
∃ (N : ℕ),
∀ j ≥ N, ∀ k ≥ N, ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θ j t x - θ k t x) ≤ η)
:
∃ (Θ : ℝ → Homogenization.Vec 2 → ℝ),
(∀ t ∈ Set.Icc 0 1, IsZ2Periodic (Θ t)) ∧ (∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (Θ t)) ∧ MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Θ p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube) ∧ ∀ (η : ℝ),
0 < η →
∃ (N : ℕ), ∀ j ≥ N, ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θ j t x - Θ t x) ≤ η
Existence of the limit profile with all its properties.