Weighted Young estimates for the actual coefficient-gradient Leibniz terms.

noncomputable def AVenhance.Infra.Section4.iterateMatrixWord (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : Matrix (Fin 2) (Fin 2) ℝ

The actual entrywise spatial derivative of a matrix coefficient.

Equations

• AVenhance.Infra.Section4.iterateMatrixWord A w x i j = AVenhance.Infra.Section4.iterateSpatialWord w (fun (y : Homogenization.Vec 2) => A y i j) x

noncomputable def AVenhance.Infra.Section4.iterateSplitFlux (P : List (List (Fin 2) × List (Fin 2))) (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

A specified list of actual Leibniz terms, retaining their multiplicities.

Equations

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

theorem AVenhance.Infra.Section4.iterateSplitFlux_eq_sum (P : List (List (Fin 2) × List (Fin 2))) (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (x : Homogenization.Vec 2) : iterateSplitFlux P A v x = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => (iterateMatrixWord A p.1 x).mulVec (spaceGrad (iterateSpatialWord p.2 v) x)) P).sum

The specified flux is exactly a sum of matrix-gradient products.

theorem AVenhance.Infra.Section4.IteratesWeightedFlux.iterate_dot_list_sum (a : Homogenization.Vec 2) (P : List (Homogenization.Vec 2)) : Homogenization.vecDot a P.sum = (List.map (Homogenization.vecDot a) P).sum

theorem AVenhance.Infra.Section4.IteratesWeightedFlux.iterate_abs_list_sum {α : Type u_1} (P : List α) (f : α → ℝ) : |(List.map f P).sum| ≤ (List.map (fun (p : α) => |f p|) P).sum

theorem AVenhance.Infra.Section4.iterate_split_flux_pairing_abs_bound (P : List (List (Fin 2) × List (Fin 2))) (A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (x a : Homogenization.Vec 2) (ρ D : List (Fin 2) × List (Fin 2) → ℝ) (hρ : ∀ p ∈ P, 0 < ρ p) (hA : ∀ p ∈ P, ∀ (i j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => A y i j) x| ≤ D p) : |Homogenization.vecDot a (iterateSplitFlux P A v x)| ≤ (List.map ρ P).sum * Homogenization.vecNormSq a + (List.map (fun (p : List (Fin 2) × List (Fin 2)) => D p ^ 2 / ρ p * Homogenization.vecNormSq (spaceGrad (iterateSpatialWord p.2 v) x)) P).sum

Weighted Young's inequality for any actual subset of the Leibniz terms. The weights allocate dissipation across terms; the remainder consists only of the actual lower scalar gradients and coefficient jet bounds.

theorem AVenhance.Infra.Section4.iterate_vecNormSq_continuous {a : Homogenization.Vec 2 → Homogenization.Vec 2} (ha : Continuous a) : Continuous fun (x : Homogenization.Vec 2) => Homogenization.vecNormSq (a x)

Continuity of the actual squared vector norm.

theorem AVenhance.Infra.Section4.IteratesWeightedFlux.iterate_continuous_list_sum {α : Type u_1} (P : List α) (f : α → Homogenization.Vec 2 → ℝ) (hf : ∀ p ∈ P, Continuous (f p)) : Continuous fun (x : Homogenization.Vec 2) => (List.map (fun (p : α) => f p x) P).sum