The q=1 integration-by-parts contribution and the higher-order energy convolution, assembled into the normalized analytic estimate.

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

noncomputable def AVenhance.Infra.Section4.thetaAnalyticInductionLevel (θ : ℝ → Homogenization.Vec 2 → ℝ) (κ : ℝ) (n : ℕ) : ℝ

Recursion level with a gradient-only order-zero base. Positive orders use the full spatial-supremum plus integrated-gradient energy level.

Equations

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

theorem AVenhance.Infra.Section4.ThetaAnalyticProof.theta_proof_sqrt_gradient_le_level {θ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} (hκ : 0 < κ) (w : List (Fin 2)) : √(thetaWordSpaceTimeGradientEnergy θ w) ≤ thetaAnalyticInductionLevel θ κ w.length / √κ

theorem AVenhance.Infra.Section4.ThetaAnalyticProof.theta_proof_abs_list_sum_le (L : List ℝ) : |L.sum| ≤ (List.map (fun (x : ℝ) => |x|) L).sum

noncomputable def AVenhance.Infra.Section4.thetaAnalyticHighConvolution {β : ℝ} {m : ℕ} (I : Ingredients β) (κ : ℝ) (θ : ℝ → Homogenization.Vec 2 → ℝ) (n : ℕ) : ℝ

Higher-order convolution of potential derivative bounds and analytic induction levels.

Equations

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

theorem AVenhance.Infra.Section4.theta_flux_pairing_split_abs_le_of_A3 {β κ : ℝ} {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 < κ) {T : ℝ} (hT : T ∈ Set.Icc 0 1) (w : List (Fin 2)) : |∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (classicalWordDerivative w (θ t)) x) (thetaStreamCommutatorFlux w ((fun (t : ℝ) => Φ (m - 1) t) t) (θ t) x)| ≤ 2 * ↑w.length * thetaPotentialDerivativeCoefficient I 2 * thetaAnalyticInductionLevel θ κ (w.length - 1) ^ 2 / κ + 2 * √(thetaIntervalWordGradientEnergy θ T w) * thetaAnalyticHighConvolution I κ θ w.length

The flux pairing is split into the q=1 square-energy term and the q≥2 Cauchy term.