The normalized analytic derivative recursion for the classical theta solution, conditional on the stream-regularity and diffusivity-recursion conclusion data.

theorem AVenhance.Infra.Section4.ThetaAnalyticRecursion.theta_analytic_energyLevel_nonneg {θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} (n : ℕ) : 0 ≤ thetaEnergyLevel θ κ n

theorem AVenhance.Infra.Section4.ThetaAnalyticRecursion.theta_analytic_inductionLevel_nonneg {θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} (n : ℕ) : 0 ≤ thetaAnalyticInductionLevel θ κ n

theorem AVenhance.Infra.Section4.theta_interval_gradient_energy_eq_full {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : thetaIntervalWordGradientEnergy θ 1 w = thetaWordSpaceTimeGradientEnergy θ w

The full space-time gradient energy is the interval energy at T = 1.

theorem AVenhance.Infra.Section4.ThetaAnalyticRecursion.theta_analytic_young {κ G H : ℝ} (hκ : 0 < κ) (hG : 0 ≤ G) : 4 * √G * H ≤ κ * G + 4 * H ^ 2 / κ

theorem AVenhance.Infra.Section4.ThetaAnalyticRecursion.theta_word_energy_step_of_A3 {β κ R₀ B : ℝ} {m : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel fun (t : ℝ) => Φ (m - 1) t) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hκ : 0 < κ) (hTrace : ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ B * (↑w.length.factorial / R₀ ^ w.length)) (w : List (Fin 2)) (hn : 1 ≤ w.length) : √(thetaWordSpatialEnergySup θ w) + √κ * √(thetaWordSpaceTimeGradientEnergy θ w) ≤ 2 * B * (↑w.length.factorial / R₀ ^ w.length) + 4 * √(↑w.length * thetaPotentialDerivativeCoefficient I 2 / κ) * thetaAnalyticInductionLevel θ κ (w.length - 1) + 4 * thetaAnalyticHighConvolution I κ θ w.length / √κ

One ordered derivative energy estimate, with the top derivative kept at the same partial time level as the differentiated energy identity.

theorem AVenhance.Infra.Section4.theta_analytic_level_recursion_of_A3 {β κ R₀ B : ℝ} {m n : ℕ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel fun (t : ℝ) => Φ (m - 1) t) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hκ : 0 < κ) (hTrace : ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, classicalWordDerivative w θ₀ x ^ 2) ≤ B * (↑w.length.factorial / R₀ ^ w.length)) (hn : 1 ≤ n) : thetaAnalyticInductionLevel θ κ n ≤ 2 * B * (↑n.factorial / R₀ ^ n) + 4 * √(↑n * thetaPotentialDerivativeCoefficient I 2 / κ) * thetaAnalyticInductionLevel θ κ (n - 1) + 4 * ∑ q ∈ Finset.range (n + 1), if 2 ≤ q then ↑(n.choose q) * (thetaPotentialDerivativeCoefficient I q / κ) * thetaAnalyticInductionLevel θ κ (n - q) else 0

Lift the ordered-word energy identity to the maximum derivative level. The zero-level value is not used here: every order in this recursion is positive, and all lower levels use the gradient-only convention.