Spatial differentiability and velocity estimates for the limit stream.

theorem AVenhance.Infra.Construction.LimitFieldRegularity.limitStreamSeq_slice_contDiff {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) : ContDiff ℝ (↑⊤) (Φ m t)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.vec_basis_decomp (v : Homogenization.Vec 2) : v = v 0 • Homogenization.basisVec 0 + v 1 • Homogenization.basisVec 1

theorem AVenhance.Infra.Construction.LimitFieldRegularity.clm_norm_le_two_basis {L : Homogenization.Vec 2 →L[ℝ] ℝ} {B : ℝ} (hB : 0 ≤ B) (h0 : ‖L (Homogenization.basisVec 0)‖ ≤ B) (h1 : ‖L (Homogenization.basisVec 1)‖ ≤ B) : ‖L‖ ≤ 2 * B

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamFDeriv_increment_norm_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) : ‖fderiv ℝ (Φ m t) x - fderiv ℝ (Φ (m - 1) t) x‖ ≤ 640 * epsilon β I.Λ m ^ (β - 1)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamFDeriv_telescope {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (m k : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : fderiv ℝ (Φ (m + k) t) x - fderiv ℝ (Φ m t) x = ∑ j ∈ Finset.range k, (fderiv ℝ (Φ (m + j + 1) t) x - fderiv ℝ (Φ (m + j) t) x)

noncomputable def AVenhance.Infra.Construction.LimitFieldRegularity.streamDerivativeTailConstant {β : ℝ} (I : Ingredients β) : ℝ

Geometric-tail constant for the stream derivative convergence estimate.

Equations

• AVenhance.Infra.Construction.LimitFieldRegularity.streamDerivativeTailConstant I = 640 / (1 - ↑I.Λ ^ (-(β - 1)))

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamDerivativeTailConstant_pos {β : ℝ} (I : Ingredients β) : 0 < streamDerivativeTailConstant I

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamFDeriv_tail_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m k : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : ‖fderiv ℝ (Φ (m + k) t) x - fderiv ℝ (Φ m t) x‖ ≤ streamDerivativeTailConstant I * epsilon β I.Λ (m + 1) ^ (β - 1)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamFDeriv_cauchySeq {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (t : ℝ) (x : Homogenization.Vec 2) : CauchySeq fun (m : ℕ) => fderiv ℝ (Φ m t) x

noncomputable def AVenhance.Infra.Construction.LimitFieldRegularity.streamFDerivLimit {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] ℝ

Limit of the spatial Fréchet derivatives of the stream sequence.

Equations

• AVenhance.Infra.Construction.LimitFieldRegularity.streamFDerivLimit hseq hreg t x = Classical.choose ⋯

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamFDerivLimit_tendsto {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (t : ℝ) (x : Homogenization.Vec 2) : Filter.Tendsto (fun (m : ℕ) => fderiv ℝ (Φ m t) x) Filter.atTop (nhds (streamFDerivLimit hseq hreg t x))

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamFDerivLimit_uniformlyOn {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (t : ℝ) : TendstoUniformlyOn (fun (m : ℕ) (x : Homogenization.Vec 2) => fderiv ℝ (Φ m t) x) (streamFDerivLimit hseq hreg t) Filter.atTop Set.univ

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamFDerivLimit_uniformlyOn_spaceTime {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) : TendstoUniformlyOn (fun (m : ℕ) (p : ℝ × Homogenization.Vec 2) => fderiv ℝ (Φ m p.1) p.2) (fun (p : ℝ × Homogenization.Vec 2) => streamFDerivLimit hseq hreg p.1 p.2) Filter.atTop Set.univ

def AVenhance.Infra.Construction.LimitFieldRegularity.rotateFDeriv (L : Homogenization.Vec 2 →L[ℝ] ℝ) : Homogenization.Vec 2

Rotate a scalar spatial differential by a quarter turn to obtain a velocity.

Equations

• AVenhance.Infra.Construction.LimitFieldRegularity.rotateFDeriv L = ![-L (Homogenization.basisVec 1), L (Homogenization.basisVec 0)]

theorem AVenhance.Infra.Construction.LimitFieldRegularity.norm_rotateFDeriv_sub_le (L K : Homogenization.Vec 2 →L[ℝ] ℝ) : ‖rotateFDeriv L - rotateFDeriv K‖ ≤ ‖L - K‖

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVel_eq_rotateFDeriv (ψ : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : streamVel ψ t x = rotateFDeriv (fderiv ℝ (ψ t) x)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.fderiv_gradient_component_eq_hessian {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 2) (x : Homogenization.Vec 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec i)) x) (Homogenization.basisVec j) = (iteratedFDeriv ℝ 2 f x) fun (k : Fin 2) => Homogenization.basisVec (if k = 0 then j else i)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVel_increment_spatial_lipschitz {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x y : Homogenization.Vec 2) : ‖streamVel (Φ m) t x - streamVel (Φ (m - 1)) t x - (streamVel (Φ m) t y - streamVel (Φ (m - 1)) t y)‖ ≤ 2 ^ 18 * epsilon β I.Λ m ^ (β - 2) * ‖x - y‖

theorem AVenhance.Infra.Construction.LimitFieldRegularity.scale_interpolation {α s e d A B q : ℝ} (hα : 0 < α) (hα1 : α < 1) (he : 0 < e) (hd : 0 ≤ d) (hq : 0 ≤ q) (hA : 0 ≤ A) (hB : 0 ≤ B) (hamp : q ≤ A * e ^ s) (hlinear : q ≤ B * e ^ (s - 1) * d) : q ≤ (A + B) * e ^ (s - α) * d ^ α

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVel_increment_norm_le {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) : ‖streamVel (Φ m) t x - streamVel (Φ (m - 1)) t x‖ ≤ 640 * epsilon β I.Λ m ^ (β - 1)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVel_increment_spatial_holder {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {α : ℝ} (hα : 0 < α) (hαβ : α < β - 1) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x y : Homogenization.Vec 2) : ‖streamVel (Φ m) t x - streamVel (Φ (m - 1)) t x - (streamVel (Φ m) t y - streamVel (Φ (m - 1)) t y)‖ ≤ (1280 + 2 ^ 18) * epsilon β I.Λ m ^ (β - 1 - α) * ‖x - y‖ ^ α

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_time_constant_nonneg {β A : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (htime : StreamVelocityTimeIncrementBound A I Φ) : 0 ≤ A

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVel_increment_time_holder {β A C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (htime : StreamVelocityTimeIncrementBound A I Φ) {α : ℝ} (hα : 0 < α) (hαβ : α < β - 1) {m : ℕ} (hm : 1 ≤ m) (s t : ℝ) (x : Homogenization.Vec 2) : ‖streamVel (Φ m) s x - streamVel (Φ (m - 1)) s x - (streamVel (Φ m) t x - streamVel (Φ (m - 1)) t x)‖ ≤ (1280 + A) * epsilon β I.Λ m ^ (β - 1 - α) * |s - t| ^ α

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVel_uniformlyOn {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) : TendstoUniformlyOn (fun (M : ℕ) (p : ℝ × Homogenization.Vec 2) => streamVel (Φ M) p.1 p.2) (fun (p : ℝ × Homogenization.Vec 2) => rotateFDeriv (streamFDerivLimit hseq hreg p.1 p.2)) Filter.atTop (Set.Icc 0 1 ×ˢ Set.univ)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamLimit_hasFDerivAt {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hlim : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (t : ℝ) (x : Homogenization.Vec 2) : HasFDerivAt (φ t) (streamFDerivLimit hseq hreg t x) x

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamLimit_differentiable {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hlim : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (t : ℝ) : Differentiable ℝ (φ t)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamLimit_velocity_eq {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hlim : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (t : ℝ) (x : Homogenization.Vec 2) : streamVel φ t x = rotateFDeriv (streamFDerivLimit hseq hreg t x)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_tendsto {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hlim : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (t : ℝ) (ht : t ∈ Set.Icc 0 1) (x : Homogenization.Vec 2) : Filter.Tendsto (fun (M : ℕ) => streamVel (Φ M) t x) Filter.atTop (nhds (streamVel φ t x))

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVel_zero_from_seq {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (t : ℝ) (x : Homogenization.Vec 2) : streamVel (Φ 0) t x = 0

theorem AVenhance.Infra.Construction.LimitFieldRegularity.sequence_telescope {G : Type u_1} [AddCommGroup G] (v : ℕ → G) (h0 : v 0 = 0) (M : ℕ) : v M = ∑ j ∈ Finset.range M, (v (j + 1) - v j)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.epsilon_holder_series_bound {β ρ : ℝ} (I : Ingredients β) (hρ : 0 < ρ) (M : ℕ) : ∑ j ∈ Finset.range M, epsilon β I.Λ (j + 1) ^ ρ ≤ epsilon β I.Λ 1 ^ ρ / (1 - ↑I.Λ ^ (-ρ))

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_spatial_partial_sum_bound {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {α ρ : ℝ} (hα : 0 < α) (hαβ : α < β - 1) (hρ : ρ = β - 1 - α) (M : ℕ) (t : ℝ) (x y : Homogenization.Vec 2) : ‖streamVel (Φ M) t x - streamVel (Φ M) t y‖ ≤ (1280 + 2 ^ 18) * ‖x - y‖ ^ α * ∑ j ∈ Finset.range M, epsilon β I.Λ (j + 1) ^ ρ

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_spatial_finite_bound {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {α ρ : ℝ} (hα : 0 < α) (hαβ : α < β - 1) (hρ : ρ = β - 1 - α) (hρpos : 0 < ρ) (M : ℕ) (t : ℝ) (x y : Homogenization.Vec 2) : ‖streamVel (Φ M) t x - streamVel (Φ M) t y‖ ≤ (1280 + 2 ^ 18) * ‖x - y‖ ^ α * (epsilon β I.Λ 1 ^ ρ / (1 - ↑I.Λ ^ (-ρ)))

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_time_partial_sum_bound {β A C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (htime : StreamVelocityTimeIncrementBound A I Φ) {α ρ : ℝ} (hα : 0 < α) (hαβ : α < β - 1) (hρ : ρ = β - 1 - α) (M : ℕ) (s t : ℝ) (x : Homogenization.Vec 2) : ‖streamVel (Φ M) s x - streamVel (Φ M) t x‖ ≤ (1280 + A) * |s - t| ^ α * ∑ j ∈ Finset.range M, epsilon β I.Λ (j + 1) ^ ρ

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_time_finite_bound {β A C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (htime : StreamVelocityTimeIncrementBound A I Φ) {α ρ : ℝ} (hα : 0 < α) (hαβ : α < β - 1) (hρ : ρ = β - 1 - α) (hρpos : 0 < ρ) (M : ℕ) (s t : ℝ) (x : Homogenization.Vec 2) : ‖streamVel (Φ M) s x - streamVel (Φ M) t x‖ ≤ (1280 + A) * |s - t| ^ α * (epsilon β I.Λ 1 ^ ρ / (1 - ↑I.Λ ^ (-ρ)))

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_spatial_holder {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hlim : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) {α : ℝ} (hα : 0 < α) (hαβ : α < β - 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x y : Homogenization.Vec 2), ‖streamVel φ t x - streamVel φ t y‖ ≤ K * ‖x - y‖ ^ α

theorem AVenhance.Infra.Construction.LimitFieldRegularity.streamVelocity_time_holder {β A C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (htime : StreamVelocityTimeIncrementBound A I Φ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hlim : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) {α : ℝ} (hα : 0 < α) (hαβ : α < β - 1) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ s ∈ Set.Icc 0 1, ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖streamVel φ s x - streamVel φ t x‖ ≤ K * |s - t| ^ α

theorem AVenhance.Infra.Construction.LimitFieldRegularity.limitField_holder_class {β A C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (htime : StreamVelocityTimeIncrementBound A I Φ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hlim : ∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) (hvelUniform : TendstoUniformlyOn (fun (M : ℕ) (p : ℝ × Homogenization.Vec 2) => streamVel (Φ M) p.1 p.2) (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) Filter.atTop (Set.Icc 0 1 ×ˢ Set.univ)) {α : ℝ} (hα : 0 < α) (hαβ : α < β - 1) : IsHolderClass α (streamVel φ)

theorem AVenhance.Infra.Construction.LimitFieldRegularity.smoothPartial {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (v : Homogenization.Vec 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (fderiv ℝ ψ x) v

theorem AVenhance.Infra.Construction.LimitFieldRegularity.partial_fderiv_eq_second {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (v w x : Homogenization.Vec 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => (fderiv ℝ ψ y) v) x) w = ((fderiv ℝ (fderiv ℝ ψ) x) w) v

theorem AVenhance.Infra.Construction.LimitFieldRegularity.limitPotential_divFree_at_time {φ : ℝ → Homogenization.Vec 2 → ℝ} (t : ℝ) (hφ : Differentiable ℝ (φ t)) (hvel : Continuous fun (x : Homogenization.Vec 2) => streamVel φ t x) (ψ : Homogenization.Vec 2 → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Homogenization.Vec 2), Homogenization.vecDot (streamVel φ t x) (spaceGrad ψ x) = 0

theorem AVenhance.Infra.Construction.limitField_pointwise_tail_differentiable_velocity {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) : ∃ (φ : ℝ → Homogenization.Vec 2 → ℝ), (∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) ∧ (∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ 11 * epsilon β I.Λ (M + 1) ^ β) ∧ (∀ (t : ℝ), Differentiable ℝ (φ t)) ∧ TendstoUniformlyOn (fun (M : ℕ) (p : ℝ × Homogenization.Vec 2) => streamVel (Φ M) p.1 p.2) (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) Filter.atTop (Set.Icc 0 1 ×ˢ Set.univ)

The pointwise limit, tail, differentiability, and uniform velocity limit consequences of the stream-regularity increment estimates.

theorem AVenhance.Infra.Construction.limitField_regular_conditional {β A C α : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (htime : StreamVelocityTimeIncrementBound A I Φ) (hα : 0 < α) (hαβ : α < β - 1) : ∃ (φ : ℝ → Homogenization.Vec 2 → ℝ), (∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) ∧ (∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ 11 * epsilon β I.Λ (M + 1) ^ β) ∧ (∀ (t : ℝ), Differentiable ℝ (φ t)) ∧ TendstoUniformlyOn (fun (M : ℕ) (p : ℝ × Homogenization.Vec 2) => streamVel (Φ M) p.1 p.2) (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) Filter.atTop (Set.Icc 0 1 ×ˢ Set.univ) ∧ IsHolderClass α (streamVel φ) ∧ IsDivFree (streamVel φ)

Conditional limit-field regularity in the form used for the limit field. The additional htime input is the time-increment estimate needed for temporal Hölder regularity; all other conclusions follow from the explicit stream-regularity bounds.