All-order material jets with a separate auxiliary spatial/word budget.

structure AVenhance.Infra.Construction.MaterialAuxJetLevels {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (N : ℕ) (K : ℝ) (cut : ℕ) : Prop

Source material/spatial jets through cut, using auxiliary budget N. The material range remains finite because time-cutoff data are only used through Nstar; spatial orders can exceed that cutoff.

• velocity (m : ℕ) (α : List (Fin 2)) (r : ℕ) : r ≤ cut → Section4.amnrMixedWord α r ≠ [] → α.length + 2 * r + 1 ≤ N → ∀ (i : Fin 2) (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2) (Section4.amnrMixedWord α r) (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2 i) z| ≤ K * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * AVenhance.a β I.Λ m ^ r
• gradient (m : ℕ) (α : List (Fin 2)) (r : ℕ) : r ≤ cut → α.length + 2 * r + 2 ≤ N → ∀ (i p : Fin 2) (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2) (Section4.amnrMixedWord α r) (Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2) i p) z| ≤ K * AVenhance.a β I.Λ m * (epsilon β I.Λ m)⁻¹ ^ α.length * AVenhance.a β I.Λ m ^ r

theorem AVenhance.Infra.Construction.material_aux_velocity_nonempty_spatial_abs_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (hne : α ≠ []) {N : ℕ} (hbudget : α.length + 1 ≤ N) (i : Fin 2) (z : Section4.AmnrSpace) : |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2) (List.map some α) (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2 i) z| ≤ Section4.amnrSpatialVelocityConstant N * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length

Spatial velocity jets at arbitrary finite auxiliary order follow from the all-order spatial displays of the stream-regularity estimates, with no bound on the velocity value.

theorem AVenhance.Infra.Construction.material_aux_jet_levels_spatial {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {N : ℕ} : ∃ (K : ℝ), 1 ≤ K ∧ MaterialAuxJetLevels I Φ N K 0

The zero material level is precisely the source spatial stream-regularity estimate.

theorem AVenhance.Infra.Construction.material_aux_fastVelocity_mixed_abs_le_of_lower_gradient_bounds {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {K : ℝ} {Nspace cut : ℕ} (hlevels : MaterialAuxJetLevels I Φ Nspace K cut) (hK : 0 ≤ K) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (n : ℕ) (hn : n ≤ cut + 1) (hcutN : cut + 1 ≤ Nstar β) (hbudget : α.length + 1 + 2 * n ≤ Nspace) (i : Fin 2) (z : Section4.AmnrSpace) : |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α n) (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2 i - streamVel (Φ (m - 1)) y.1 y.2 i) z| ≤ (1 + 2 ^ (Nspace + 1) * K) ^ n * materialAuxStreamMixedCurrentConstant I Nspace * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ n

Fast velocity mixed jets use the differentiated recursion and lower material-gradient jets, with the source material order kept at Nstar.

noncomputable def AVenhance.Infra.Construction.materialAuxHigherFastConstant {β : ℝ} (I : Ingredients β) (K : ℝ) (N : ℕ) : ℝ

Uniform fast-velocity constant for the auxiliary material word budget.

Equations

• AVenhance.Infra.Construction.materialAuxHigherFastConstant I K N = max 1 ((1 + 2 ^ (N + 1) * K) ^ N * AVenhance.Infra.Construction.materialAuxStreamMixedCurrentConstant I N)

theorem AVenhance.Infra.Construction.materialAuxHigherFastConstant_one_le {β K : ℝ} (I : Ingredients β) (N : ℕ) : 1 ≤ materialAuxHigherFastConstant I K N

noncomputable def AVenhance.Infra.Construction.materialAuxHigherVelocityStepConstant {β : ℝ} (I : Ingredients β) (K : ℝ) (N n k : ℕ) : ℝ

Scale-step constant for changing the velocity in a material word.

Equations

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

theorem AVenhance.Infra.Construction.materialAuxHigherVelocityStepConstant_nonneg {β K : ℝ} (I : Ingredients β) (hK : 0 ≤ K) (N n k : ℕ) : 0 ≤ materialAuxHigherVelocityStepConstant I K N n k

theorem AVenhance.Infra.Construction.material_aux_velocity_higher_source_step {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {Nspace n m : ℕ} {K : ℝ} (hn : 1 ≤ n) (hnN : n ≤ Nstar β) (hlevels : MaterialAuxJetLevels I Φ Nspace K (n - 1)) (hK : 1 ≤ K) (α : List (Fin 2)) (hbudget : α.length + 2 * n + 1 ≤ Nspace) (hm : 1 ≤ m) (i : Fin 2) (z : Section4.AmnrSpace) : |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) ((Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2) (List.replicate n none) fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2 i) - Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.replicate n none) fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2 i) z| ≤ materialAuxHigherVelocityStepConstant I K Nspace n α.length * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ n

One higher source material order follows from strictly lower velocity and gradient levels plus the all-order transported fast increment.

theorem AVenhance.Infra.Construction.material_aux_velocity_higher_material_abs_le_of_source_lower_levels {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {Nspace n : ℕ} {K : ℝ} (hn : 1 ≤ n) (hnN : n ≤ Nstar β) (hlevels : MaterialAuxJetLevels I Φ Nspace K (n - 1)) (hK : 1 ≤ K) (m : ℕ) (α : List (Fin 2)) (hbudget : α.length + 2 * n + 1 ≤ Nspace) (i : Fin 2) (z : Section4.AmnrSpace) : |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2) (Section4.amnrMixedWord α n) (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2 i) z| ≤ 2 * materialAuxHigherVelocityStepConstant I K Nspace n α.length * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ n

The higher material velocity jets telescope over scales. Their exponent is uniformly negative, so the new constant is independent of the scale.

noncomputable def AVenhance.Infra.Construction.materialAuxVelocityAdvanceConstant {β : ℝ} (I : Ingredients β) (K : ℝ) (N cut : ℕ) : ℝ

The source constant after one auxiliary material induction level.

Equations

• AVenhance.Infra.Construction.materialAuxVelocityAdvanceConstant I K N cut = K + 2 * AVenhance.Infra.Construction.materialAuxHigherVelocityStepConstant I K N (cut + 1) N

theorem AVenhance.Infra.Construction.materialAuxVelocityAdvanceConstant_nonneg {β K : ℝ} (I : Ingredients β) (hK : 0 ≤ K) (N cut : ℕ) : 0 ≤ materialAuxVelocityAdvanceConstant I K N cut

theorem AVenhance.Infra.Construction.materialAuxHigherVelocityStepConstant_mono_spatial {β K : ℝ} (I : Ingredients β) (hK : 0 ≤ K) (N n : ℕ) {k l : ℕ} (hkl : k ≤ l) : materialAuxHigherVelocityStepConstant I K N n k ≤ materialAuxHigherVelocityStepConstant I K N n l

theorem AVenhance.Infra.Construction.material_aux_velocity_advance {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {N cut : ℕ} {K : ℝ} (hlevels : MaterialAuxJetLevels I Φ N K cut) (hK : 1 ≤ K) (hcutN : cut + 1 ≤ Nstar β) (m : ℕ) (α : List (Fin 2)) (r : ℕ) (hr : r ≤ cut + 1) (hne : Section4.amnrMixedWord α r ≠ []) (hbudget : α.length + 2 * r + 1 ≤ N) (i : Fin 2) (z : Section4.AmnrSpace) : |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2) (Section4.amnrMixedWord α r) (fun (y : Section4.AmnrSpace) => streamVel (Φ m) y.1 y.2 i) z| ≤ materialAuxVelocityAdvanceConstant I K N cut * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ r

Extend the velocity part of the source invariant through its next material order, summing the actual scale increments.

noncomputable def AVenhance.Infra.Construction.materialAuxJetAdvanceConstant {β : ℝ} (I : Ingredients β) (K : ℝ) (N cut : ℕ) : ℝ

Advancing one material level closes the gradient estimates from the velocity estimates at that same level and the previous gradient level.

Equations

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

theorem AVenhance.Infra.Construction.material_aux_jet_levels_advance {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {N cut : ℕ} {K : ℝ} (hlevels : MaterialAuxJetLevels I Φ N K cut) (hK : 1 ≤ K) (hcutN : cut + 1 ≤ Nstar β) : ∃ (Knew : ℝ), 1 ≤ Knew ∧ MaterialAuxJetLevels I Φ N Knew (cut + 1)

theorem AVenhance.Infra.Construction.material_aux_jet_levels_all_orders_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) : ∃ (K : ℝ), 1 ≤ K ∧ MaterialAuxJetLevels I Φ (2 * Nstar β + 1) K (Nstar β)

The differentiated recursion and the actual stream-regularity spatial estimates give all source word bounds through the paper's material cutoff. The auxiliary word budget is 2*Nstar+1; time derivatives of recursion cutoffs never exceed the literal Nstar.