Honest energy recursion and analytic bounds for the classical theta solution, conditional only on the stream-regularity and diffusivity-recursion conclusion data.

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_list_fun_sum_apply {α : Type u_1} (L : List (α → ℝ)) (x : α) : L.sum x = (List.map (fun (f : α → ℝ) => f x) L).sum

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_continuous_fun_list_sum {α : Type u_1} [TopologicalSpace α] (L : List (α → ℝ)) (hL : ∀ f ∈ L, Continuous f) : Continuous L.sum

noncomputable def AVenhance.Infra.Section4.thetaHonestResidualTermExtension (φ θ : ℝ → Homogenization.Vec 2 → ℝ) (split : List (Fin 2) × List (Fin 2)) (j : Fin 2) (p : ℝ × Homogenization.Vec 2) : ℝ

One differentiated-drift term in the joint space-time representation of the transport commutator.

Equations

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

noncomputable def AVenhance.Infra.Section4.thetaHonestResidualExtension (φ θ : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : ℝ

Joint continuous representative of the differentiated transport commutator.

Equations

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

theorem AVenhance.Infra.Section4.thetaHonestResidualExtension_continuous {φ θ : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (hφ : ContDiffOn ℝ (↑⊤) (Function.uncurry φ) (Set.Ici 0 ×ˢ Set.univ)) (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) : Continuous (thetaHonestResidualExtension φ θ w)

theorem AVenhance.Infra.Section4.thetaHonestResidualExtension_eq_commutator {φ θ : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (hφ : ContDiffOn ℝ (↑⊤) (Function.uncurry φ) (Set.Ici 0 ×ˢ Set.univ)) (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : thetaHonestResidualExtension φ θ w (t, x) = classicalWordDerivative w (classicalTransport (streamVel (fun (x : ℝ) => φ t) 0) (θ t)) x - Homogenization.vecDot (streamVel (fun (x : ℝ) => φ t) 0 x) (spaceGrad (classicalWordDerivative w (θ t)) x)

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

The coefficient supplied by the high-order stream-regularity barNorm bound for a split with q derivatives on the drift.

Equations

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

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

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_residual_term_integral_bound_of_A3 {β : ℝ} {m : ℕ} {κ T : ℝ} (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 < κ) (hT : T ∈ Set.Icc 0 1) {w : List (Fin 2)} (split : List (Fin 2) × List (Fin 2)) (j : Fin 2) (hleft : 1 ≤ split.1.length) : |∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, thetaWordExtension θ w p * thetaHonestResidualTermExtension (fun (t : ℝ) => Φ (m - 1) t) θ split j p| ≤ thetaHonestDriftCoefficient I split.1.length * √(thetaWordSpatialEnergySup θ w) * thetaEnergyLevel θ κ split.2.length / √κ

def AVenhance.Infra.Section4.ThetaHonestRecursion.thetaResidualClosedCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell for the temperature residual recursion.

Equations

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

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.thetaResidualClosedCell_compact : IsCompact thetaResidualClosedCell

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_residual_interval_subset_closedCell {T : ℝ} (hT : T ∈ Set.Icc 0 1) : Set.Ioo 0 T ×ˢ unitCube ⊆ thetaResidualClosedCell

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_residual_interval_integrable {T : ℝ} (hT : T ∈ Set.Icc 0 1) {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Set.Ioo 0 T ×ˢ unitCube) MeasureTheory.volume

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_abs_list_sum_le (L : List ℝ) : |L.sum| ≤ (List.map (fun (a : ℝ) => |a|) L).sum

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_list_sum_right_factor {α : Type u_1} (L : List α) (f : α → ℝ) (c : ℝ) : (List.map (fun (a : α) => f a * c) L).sum = (List.map f L).sum * c

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_residual_pairing_abs_le_of_A3 {β : ℝ} {m : ℕ} {κ T : ℝ} (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 < κ) (hT : T ∈ Set.Icc 0 1) (w : List (Fin 2)) : |∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, thetaWordExtension θ w p * thetaHonestResidualExtension (fun (t : ℝ) => Φ (m - 1) t) θ w p| ≤ 2 * √(thetaWordSpatialEnergySup θ w) * ∑ q ∈ Finset.range (w.length + 1), ↑(if q = 0 then 0 else w.length.choose q) * (thetaHonestDriftCoefficient I q * thetaEnergyLevel θ κ (w.length - q) / √κ)

The complete commutator pairing on a partial time interval, bounded by the stream-regularity Leibniz convolution and the lower energy levels.

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

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_driftCoefficient_nonneg {β : ℝ} {m q : ℕ} (I : Ingredients β) : 0 ≤ thetaHonestDriftCoefficient I q

theorem AVenhance.Infra.Section4.ThetaHonestRecursion.theta_word_energy_bound_of_A3 {β : ℝ} {m : ℕ} {κ R 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 < κ) (hθ₀ : IsThetaAnalytic R θ₀) (hN : N = √(l2NormSq θ₀)) (w : List (Fin 2)) : √(thetaWordSpatialEnergySup θ w) + √κ * √(thetaWordSpaceTimeGradientEnergy θ w) ≤ 8 * (N * (↑w.length.factorial / R ^ w.length) + ∑ q ∈ Finset.range (w.length + 1), ↑(if q = 0 then 0 else w.length.choose q) * (thetaHonestDriftCoefficient I q * thetaEnergyLevel θ κ (w.length - q) / √κ))

One ordered derivative's energy estimate after inserting the stream-regularity barNorm conclusion. The commutator is paired in space-time and Cauchy-- Schwarz is applied before Young's inequality, so the conclusion records the larger honest convolution cost.

theorem AVenhance.Infra.Section4.theta_order_zero_energy_bound {κ N : ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (hsol : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (hκ : 0 < κ) (hN : N = √(l2NormSq θ₀)) : thetaEnergyLevel θ κ 0 ≤ 2 * N