Honest analytic estimates for the classical theta solution.

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

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.theta_word_spatial_energy_range_bddAbove {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (w : List (Fin 2)) : BddAbove (Set.range fun (t : { t : ℝ // t ∈ Set.Icc 0 1 }) => thetaWordSpatialEnergy θ w ↑t)

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.theta_word_spatial_energy_nonneg (θ : ℝ → Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (t : ℝ) : 0 ≤ thetaWordSpatialEnergy θ w t

def AVenhance.Infra.Section4.ThetaHonestAnalytic.thetaHonestClosedCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell for the analytic induction estimates.

Equations

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

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.thetaHonestClosedCell_compact : IsCompact thetaHonestClosedCell

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.thetaHonestTimeCube_subset_closedCell : timeCube ⊆ thetaHonestClosedCell

noncomputable def AVenhance.Infra.Section4.thetaIntervalWordGradientEnergy (θ : ℝ → Homogenization.Vec 2 → ℝ) (T : ℝ) (w : List (Fin 2)) : ℝ

The gradient energy of one ordered derivative over the initial time interval [0,T].

Equations

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

theorem AVenhance.Infra.Section4.theta_interval_word_l2_le_gradient {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) {T : ℝ} (hT : T ∈ Set.Icc 0 1) {i : Fin 2} (word right : List (Fin 2)) (hperm : word.Perm (i :: right)) : ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, thetaWordExtension θ word p ^ 2 ≤ thetaWordSpaceTimeGradientEnergy θ right

theorem AVenhance.Infra.Section4.theta_intervalCube_integral_eq_interval_integral {T : ℝ} (hT : T ∈ Set.Icc 0 1) {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) : ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, f p = ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, f (t, x)

theorem AVenhance.Infra.Section4.theta_interval_word_l2_le_partial_gradient {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ)) {T : ℝ} (hT : T ∈ Set.Icc 0 1) {i : Fin 2} (word right : List (Fin 2)) (hperm : word.Perm (i :: right)) : ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, thetaWordExtension θ word p ^ 2 ≤ thetaIntervalWordGradientEnergy θ T right

On a partial time interval, a coordinate derivative is controlled by the gradient energy of the complementary word on that same interval.

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.theta_intervalCube_integral_rescale_eq {T : ℝ} (hT : T ∈ Set.Icc 0 1) {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) : ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, f p = T * ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f (T * p.1, p.2)

theorem AVenhance.Infra.Section4.theta_intervalCube_integral_mul_bounded_le {T M : ℝ} (hT : T ∈ Set.Icc 0 1) {f g a : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) (ha : Continuous a) (hM : 0 ≤ M) (haM : ∀ p ∈ Set.Ioo 0 T ×ˢ unitCube, |a p| ≤ M) : |∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, f p * (a p * g p)| ≤ M * √(∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, f p ^ 2) * √(∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, g p ^ 2)

theorem AVenhance.Infra.Section4.theta_word_spatial_energy_le_sup_of_classical {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (w : List (Fin 2)) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : thetaWordSpatialEnergy θ w t ≤ thetaWordSpatialEnergySup θ w

theorem AVenhance.Infra.Section4.theta_word_spacetime_l2_le_spatial_sup {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) (w : List (Fin 2)) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, thetaWordExtension θ w p ^ 2 ≤ thetaWordSpatialEnergySup θ w

theorem AVenhance.Infra.Section4.theta_interval_word_l2_le_spatial_sup {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ) {T : ℝ} (hT : T ∈ Set.Icc 0 1) (w : List (Fin 2)) : ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, thetaWordExtension θ w p ^ 2 ≤ thetaWordSpatialEnergySup θ w

Partial-time L² control of an order-n derivative by its uniform-time spatial energy.

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.theta_const_time_gradient_energy {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (w : List (Fin 2)) : thetaWordSpaceTimeGradientEnergy (fun (x : ℝ) => u) w = ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (classicalWordDerivative w u) x)

theorem AVenhance.Infra.Section4.theta_vecDot_list_sum (v : Homogenization.Vec 2) (L : List (Homogenization.Vec 2)) : Homogenization.vecDot v L.sum = (List.map (fun (z : Homogenization.Vec 2) => Homogenization.vecDot v z) L).sum

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

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.theta_commutator_split_count (w : List (Fin 2)) (q : ℕ) : List.count q (List.map (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length) (classicalWordCommutatorSplits w)) = if q = 0 then 0 else w.length.choose q

theorem AVenhance.Infra.Section4.theta_commutator_split_weighted_sum (w : List (Fin 2)) (F : ℕ → ℝ) : (List.map (fun (p : List (Fin 2) × List (Fin 2)) => F p.1.length) (classicalWordCommutatorSplits w)).sum = ∑ q ∈ Finset.range (w.length + 1), ↑(if q = 0 then 0 else w.length.choose q) * F q

theorem AVenhance.Infra.Section4.theta_intervalCube_list_sum_continuous (L : List (ℝ × Homogenization.Vec 2 → ℝ)) (hcont : ∀ f ∈ L, Continuous f) : Continuous fun (p : ℝ × Homogenization.Vec 2) => (List.map (fun (f : ℝ × Homogenization.Vec 2 → ℝ) => f p) L).sum

theorem AVenhance.Infra.Section4.theta_intervalCube_integral_list_sum {T : ℝ} (hT : T ∈ Set.Icc 0 1) (L : List (ℝ × Homogenization.Vec 2 → ℝ)) (hcont : ∀ f ∈ L, Continuous f) : ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, (List.map (fun (f : ℝ × Homogenization.Vec 2 → ℝ) => f p) L).sum = (List.map (fun (f : ℝ × Homogenization.Vec 2 → ℝ) => ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, f p) L).sum

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.theta_list_eval_sum_continuous (L : List (Homogenization.Vec 2 → ℝ)) (hcont : ∀ f ∈ L, Continuous f) : Continuous fun (x : Homogenization.Vec 2) => (List.map (fun (f : Homogenization.Vec 2 → ℝ) => f x) L).sum

theorem AVenhance.Infra.Section4.ThetaHonestAnalytic.theta_integral_list_sum (L : List (Homogenization.Vec 2 → ℝ)) (hcont : ∀ f ∈ L, Continuous f) : ∫ (x : Homogenization.Vec 2) in unitCube, (List.map (fun (f : Homogenization.Vec 2 → ℝ) => f x) L).sum = (List.map (fun (f : Homogenization.Vec 2 → ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, f x) L).sum

theorem AVenhance.Infra.Section4.theta_interval_stream_split_pairing_abs_le {u φ : ℝ → Homogenization.Vec 2 → ℝ} {w : List (Fin 2)} (hu : ContDiffOn ℝ (↑⊤) (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ)) (hφ : ContDiffOn ℝ (↑⊤) (Function.uncurry φ) (Set.Ici 0 ×ˢ Set.univ)) {T M : ℝ} (hT : T ∈ Set.Icc 0 1) (split : List (Fin 2) × List (Fin 2)) (hM : 0 ≤ M) (hcoef : ∀ p ∈ Set.Ioo 0 T ×ˢ unitCube, |thetaWordExtension φ split.1 p| ≤ M) : |∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, Homogenization.vecDot (thetaWordGradientExtension u w p) fun (j : Fin 2) => thetaWordExtension φ split.1 p * thetaStreamWordExtension u split.2 p j| ≤ 2 * M * √(thetaIntervalWordGradientEnergy u T w) * √(thetaIntervalWordGradientEnergy u T split.2)

A single stream-form Leibniz split on an arbitrary initial time interval. The coefficient bound is only needed on the open interval of integration.

theorem AVenhance.Infra.Section4.theta_first_order_stream_split_pairing_time_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)) (hsplit : split ∈ classicalWordCommutatorSplits w) (hlen : split.1.length = 1) : |∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo 0 T ×ˢ unitCube, Homogenization.vecDot (thetaWordGradientExtension θ w p) fun (j : Fin 2) => thetaWordExtension (fun (t : ℝ) => Φ (m - 1) t) split.1 p * thetaStreamWordExtension θ split.2 p j| ≤ 2 * (2 ^ 5 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ↑(Nat.factorial 2) * (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹) ^ 2) * ∫ (t : ℝ) in 0..T, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (classicalWordDerivative split.2 (θ t)) x)

The one-derivative stream-flux term admits the sharper energy bound after periodic integration by parts. The derivative on the top word is a coordinate derivative of the complementary word, so the resulting square is controlled by the lower-order gradient energy.

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

The joint continuous representative of one split in the differentiated stream flux.

Equations

• AVenhance.Infra.Section4.thetaStreamSplitExtension φ u split p j = AVenhance.Infra.Section4.thetaWordExtension φ split.1 p * AVenhance.Infra.Section4.thetaStreamWordExtension u split.2 p j

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

Space-time integration commutes with the finite differentiated-flux expansion.