Finite convex-combination bounds for the transition flux.
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_finite_mixture_distortion
{κ : Type u_1}
{ι : Type u_2}
(U : Finset κ)
(S : Finset ι)
(wk : κ → ℝ)
(wl : ι → ℝ)
(A : ι → Matrix (Fin 2) (Fin 2) ℝ)
(B : κ → Matrix (Fin 2) (Fin 2) ℝ)
(v : Homogenization.Vec 2)
(η : ℝ)
(hwk : ∀ k ∈ U, 0 ≤ wk k)
(hsumk : ∑ k ∈ U, wk k = 1)
(hwl : ∀ l ∈ S, 0 ≤ wl l)
(hsuml : ∑ l ∈ S, wl l = 1)
(hclose : ∀ k ∈ U, ∀ l ∈ S, ∀ (i j : Fin 2), |(A l - B k) i j| ≤ η / 2)
(hη : 0 ≤ η)
:
Homogenization.vecNormSq (∑ k ∈ U, wk k • ∑ l ∈ S, wl l • (A l - B k).mulVec v) ≤ η ^ 2 * Homogenization.vecNormSq v
Two successive finite convex averages preserve the entrywise flow distortion bound, with the sharp two-dimensional Euclidean square constant.
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_xFlowInv_right_inverse_at
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(l : ℤ)
(t : ℝ)
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_defect_eq_finite_mixture
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(hm : 1 ≤ m)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(hT : ContDiff ℝ 1 (T t))
(x : Homogenization.Vec 2)
:
The two cutoff partitions turn the defect into a finite double convex average of differences of flow Jacobians.
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_vecNormSq_smul
(c : ℝ)
(v : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_flowGrad_one_eq
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(l : ℤ)
(t : ℝ)
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Section5.r46Flux_pointwise_sq_le_of_flowBounds
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(Cmat : ℝ)
(hflow : FlowBoundsData I Φ hΦ Cmat)
(m : ℕ)
(hm : 1 ≤ m)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
{t : ℝ}
(hT : ContDiff ℝ 1 (T t))
(x : Homogenization.Vec 2)
:
Actual pointwise flux bound from stream-function estimates flow_close. On refresh windows
the defect vanishes exactly; off them the odd-mode flux is molecular, and the
two cutoff partitions average Jacobian differences.
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_slice_contDiff
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
{t : ℝ}
(ht : 0 ≤ t)
:
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_spaceGrad_continuous
{u : Homogenization.Vec 2 → ℝ}
(hu : ContDiff ℝ (↑⊤) u)
:
Continuous (spaceGrad u)
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_gradient_continuousOn
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
:
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2) (Set.Icc 0 1 ×ˢ Set.univ)
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_gradNormSq_continuousOn
{T : ℝ → Homogenization.Vec 2 → ℝ}
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
:
ContinuousOn (fun (t : ℝ) => gradNormSq fun (x : Homogenization.Vec 2) => spaceGrad (T t) x) (Set.Icc 0 1)
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46_lintegrand_eq
{F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(t : ℝ)
:
theorem
AVenhance.Infra.Section5.R46FluxEstimate.r46TimeL2_eq_lintegral
(F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Section5.r46TimeL2_gradient_eq_spaceTime
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
:
(r46TimeL2 fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T t) x) = ENNReal.ofReal √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T t) x)
The source n=0 energy norm is the same slice norm as the one consumed by
the R46 time estimate. Joint smoothness gives the Fubini identification.
theorem
AVenhance.Infra.Section5.gradNormSq_r46Flux_sq_le_of_flowBounds
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(Cmat : ℝ)
(hflow : FlowBoundsData I Φ hΦ Cmat)
(m : ℕ)
(hm : 1 ≤ m)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(t : ℝ)
(ht : 0 ≤ t)
(hF : ContDiff ℝ (↑⊤) (r46Flux I hΦ m κm T t))
:
gradNormSq (r46Flux I hΦ m κm T t) ≤ (κm * epsilon β I.Λ (m - 1) ^ (2 * delta β)) ^ 2 * gradNormSq fun (x : Homogenization.Vec 2) => spaceGrad (T t) x
Spatial integration preserves the sharp pointwise estimate.
theorem
AVenhance.Infra.Section5.r46TimeL2_flux_le_of_flowBounds
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(Cmat : ℝ)
(hflow : FlowBoundsData I Φ hΦ Cmat)
(m : ℕ)
(hm : 1 ≤ m)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ))
(hF : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (r46Flux I hΦ m κm T t))
(hκm : 0 ≤ κm)
:
The actual stream-function flow estimate gives the sharp R46 flux-to-gradient
space-time bound, with the stronger intermediate exponent 2δ.