Analytic estimates for the classical theta solution, conditional on the stream-regularity and diffusivity-recursion estimates.

theorem AVenhance.Infra.Section4.ThetaAnalyticEstimate.theta_analytic_vecList_sum_apply (L : List (Homogenization.Vec 2)) (j : Fin 2) : L.sum j = (List.map (fun (v : Homogenization.Vec 2) => v j) L).sum

def AVenhance.Infra.Section4.ThetaAnalyticEstimate.thetaAnalyticClosedCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell for the temperature analyticity estimate.

Equations

• AVenhance.Infra.Section4.ThetaAnalyticEstimate.thetaAnalyticClosedCell = Set.Icc 0 1 ×ˢ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section4.ThetaAnalyticEstimate.theta_analytic_closedCell_compact : IsCompact thetaAnalyticClosedCell

theorem AVenhance.Infra.Section4.ThetaAnalyticEstimate.theta_timeCube_subset_analyticClosedCell : timeCube ⊆ thetaAnalyticClosedCell

noncomputable def AVenhance.Infra.Section4.thetaPotentialDerivativeCoefficient {β : ℝ} {m : ℕ} (I : Ingredients β) (q : ℕ) : ℝ

The pointwise coefficient for an order-q derivative of the stream potential, copied from the stream-regularity barNorm conclusion after the factorial and radius weights are unpacked.

Equations

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

theorem AVenhance.Infra.Section4.theta_higher_order_stream_split_pairing_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) θ₀ θ) {T : ℝ} (hT : T ∈ Set.Icc 0 1) {w : List (Fin 2)} (split : List (Fin 2) × List (Fin 2)) (hq : 2 ≤ split.1.length) : |∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, Homogenization.vecDot (thetaWordGradientExtension θ w p) (thetaStreamSplitExtension (fun (t : ℝ) => Φ (m - 1) t) θ split p)| ≤ 2 * thetaPotentialDerivativeCoefficient I split.1.length * √(thetaIntervalWordGradientEnergy θ T w) * √(thetaIntervalWordGradientEnergy θ T split.2)

For q at least two, the direct stream-flux estimate controls the differentiated energy pairing by the qth coefficient and the two gradient energies.

theorem AVenhance.Infra.Section4.theta_interval_word_gradient_energy_le {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) {T : ℝ} (hT : T ∈ Set.Icc 0 1) (w : List (Fin 2)) : ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (classicalWordDerivative w (θ t)) x) ≤ thetaWordSpaceTimeGradientEnergy θ w

The gradient energy on an initial subinterval is bounded by the full space-time gradient energy.

theorem AVenhance.Infra.Section4.theta_classical_flux_interval_integral_eq_split_sum {φ θ : ℝ → Homogenization.Vec 2 → ℝ} {T : ℝ} (hT : T ∈ Set.Icc 0 1) (hφ : ContDiffOn ℝ (↑⊤) (Function.uncurry φ) (Set.Ici 0 ×ˢ Set.univ)) (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (classicalWordDerivative w (θ t)) x) (thetaStreamCommutatorFlux w (φ t) (θ t) x) = (List.map (fun (split : List (Fin 2) × List (Fin 2)) => ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, Homogenization.vecDot (thetaWordGradientExtension θ w p) (thetaStreamSplitExtension φ θ split p)) (classicalWordCommutatorSplits w)).sum

The time-integrated flux term in the differentiated energy identity is the sum of the continuous representatives of its Leibniz splits.