Passing to the limit in the weak form

If weak solutions with diffusivities κ j → 0 converge uniformly in L²(cell) to Θ, then Θ satisfies the divergence-form transport identity, has weakly continuous pairings, and bounded energy.

theorem AVenhance.Infra.FullTheorem.TransportLimit.l2_pairing_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : |∫ (p : α), f p * g p ∂μ| ≤ √(∫ (p : α), f p ^ 2 ∂μ) * √(∫ (p : α), g p ^ 2 ∂μ)

theorem AVenhance.Infra.FullTheorem.TransportLimit.l2NormSq_sub_le {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : (l2NormSq fun (x : Homogenization.Vec 2) => f x - g x) ≤ 2 * l2NormSq f + 2 * l2NormSq g

theorem AVenhance.Infra.FullTheorem.TransportLimit.limit_l2_bound {θ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {Θ : ℝ → Homogenization.Vec 2 → ℝ} (hmem : ∀ (j : ℕ), ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (θ j t)) (hbd : ∀ (j : ℕ), ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, l2NormSq (θ j t) ≤ C) (hΘ : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (Θ t)) (hunif : ∀ (η : ℝ), 0 < η → ∃ (N : ℕ), ∀ j ≥ N, ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θ j t x - Θ t x) ≤ η) : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, l2NormSq (Θ t) ≤ C

Bounded energy of the limit.

theorem AVenhance.Infra.FullTheorem.TransportLimit.limit_weak_continuity {θ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {Θ : ℝ → Homogenization.Vec 2 → ℝ} (hmem : ∀ (j : ℕ), ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (θ j t)) (hΘ : ∀ t ∈ Set.Icc 0 1, Homogenization.MemL2On unitCube (Θ t)) (hcont : ∀ (j : ℕ) (ψ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) ψ → IsZ2Periodic ψ → ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, θ j t x * ψ x) (Set.Icc 0 1)) (hunif : ∀ (η : ℝ), 0 < η → ∃ (N : ℕ), ∀ j ≥ N, ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θ j t x - Θ t x) ≤ η) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψp : IsZ2Periodic ψ) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, Θ t x * ψ x) (Set.Icc 0 1)

Weak continuity of the limit's pairings with smooth periodic functions.