Iterates Theta Source Bound

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_norm_le_energy_components {e g κ H : ℝ} (he : 0 ≤ e) (hg : 0 ≤ g) (hκ : 0 ≤ κ) (hH : 0 ≤ H) (hbound : √e + √κ * √g ≤ H) : e ≤ H ^ 2 ∧ κ * g ≤ H ^ 2

Component energies can be extracted without taking a supremum or assuming an energy identity.