Actual selected flux square from scalar gradient energies.

theorem AVenhance.Infra.Section4.iterate_filtered_flux_energy_bound {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : ℝ → Homogenization.Vec 2 → ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (q : ℕ → Bool) (hcoef : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w), ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) p.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (D E : ℕ → ℝ) (hD : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w), ∀ (j k : Fin 2), |iterateMatrixWord (A t) p.1 x j k| ≤ D p.1.length) (hE : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ E p.2.length) : (spaceTimeGradNormSq fun (t : ℝ) => iterateSplitFlux (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => q p.1.length) (iterateSpatialSplits w)) (A t) (v t)) ≤ 8 * ∑ j ∈ Finset.range (w.length + 1), if q j = true then ↑(w.length.choose j) ^ 2 * 2 ^ j * D j ^ 2 * E (w.length - j) else 0

The integrated differentiated flux is controlled directly by lower scalar L2 gradient energies. A pointwise scalar analytic bound is unnecessary.