Time regularity ingredients for the limit stream.

The flow/material estimates of §2 are carried as explicit source-form data; the recursion estimate differentiates the finite-overlap stream update and then applies the mean-value theorem in time.

noncomputable def AVenhance.constructionFlow {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

The canonical smooth periodic flow associated with one member of a stream sequence.

Equations

• AVenhance.constructionFlow hseq m = AVenhance.flow (AVenhance.streamVel (Φ m)) ⋯ ⋯

noncomputable def AVenhance.constructionFlowInv {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

The inverse-flow map for constructionFlow, with arguments ordered as in the flowInv.

Equations

• AVenhance.constructionFlowInv hseq m = AVenhance.flowInv (AVenhance.streamVel (Φ m)) ⋯ ⋯

noncomputable def AVenhance.constructionFlowJacobian {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (t s : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

The spatial Jacobian of the mth flow at offset t from start time s.

Equations

• AVenhance.constructionFlowJacobian hseq m t s x = fderiv ℝ (fun (y : Homogenization.Vec 2) => AVenhance.constructionFlow hseq m (s + t) y s) x

noncomputable def AVenhance.constructionFlowInvJacobian {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (t s : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

The spatial Jacobian of the inverse flow at offset t from start time s.

Equations

• AVenhance.constructionFlowInvJacobian hseq m t s x = fderiv ℝ (fun (y : Homogenization.Vec 2) => AVenhance.constructionFlowInv hseq m (s + t) y s) x

noncomputable def AVenhance.constructionComposedFlowJacobian {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (s r : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

The forward spatial Jacobian pulled back by its inverse, as in c.material.DX.Xinv and c.flowreg display 2.

Equations

• AVenhance.constructionComposedFlowJacobian hseq m s r x = AVenhance.constructionFlowJacobian hseq m r s (AVenhance.constructionFlowInv hseq m (s + r) x s)

noncomputable def AVenhance.flowJacobianBarNorm (n : ℕ) (R : ℝ) (J : Homogenization.Vec 2 → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) : ENNReal

Componentwise version of the source spatial seminorm for a matrix field. Each entry is measured by the scalar barNorm.

Equations

• AVenhance.flowJacobianBarNorm n R J = ⨆ (i : Fin 2), ⨆ (j : Fin 2), AVenhance.barNorm n R fun (x : Homogenization.Vec 2) => (J x) (Homogenization.basisVec j) i

noncomputable def AVenhance.constructionMaterialDerivative (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (F : ℝ → Homogenization.Vec 2 → ℝ) : ℝ → Homogenization.Vec 2 → ℝ

One material derivative along a time-dependent vector field, matching D_{t,m} = ∂ₜ + b_m·∇ in the source.

Equations

• AVenhance.constructionMaterialDerivative b F t x = deriv (fun (r : ℝ) => F r x) t + (fderiv ℝ (F t) x) (b t x)

def AVenhance.constructionMaterialIterate (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℕ → (ℝ → Homogenization.Vec 2 → ℝ) → ℝ → Homogenization.Vec 2 → ℝ

Iterates of the source material derivative.

Equations

• AVenhance.constructionMaterialIterate b 0 x✝ = x✝
• AVenhance.constructionMaterialIterate b n.succ x✝ = AVenhance.constructionMaterialDerivative b (AVenhance.constructionMaterialIterate b n x✝)

structure AVenhance.FlowBoundsData {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hseq : IsStreamSeq I Φ) (Cmat : ℝ) : Prop

Explicit source-form flow and material bounds used in the differentiated stream recursion. The seminorm fields transcribe e.Xm.regbounds and all four displays of c.flowreg componentwise; material_jacobian transcribes c.material.DX.Xinv. The final field records e.PDE.backwards for the inverse flow.

• material_constant_ge_one : 1 ≤ Cmat

  The source constant in c.material.DX.Xinv is at least one.

• inverse_regbounds (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ∀ (n : ℕ), (flowJacobianBarNorm n (2 ^ 11 * (epsilon β I.Λ m)⁻¹) fun (x : Homogenization.Vec 2) => constructionFlowInvJacobian hseq m t s x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) ≤ ENNReal.ofReal (2 ^ 23 * |t| * AVenhance.a β I.Λ m)

  e.Xm.regbounds, componentwise for every derivative order n.

• flow_close (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ∀ (x : Homogenization.Vec 2), ‖constructionFlowJacobian hseq m t s x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)‖ ≤ 2 ^ 23 * |t| * AVenhance.a β I.Λ m ∧ 2 ^ 23 * |t| * AVenhance.a β I.Λ m ≤ 1 / 4

  c.flowreg display e.Xm.bound.1.

• flow_jacobian_composed (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ∀ (n : ℕ), (flowJacobianBarNorm n (2 ^ 10 * (epsilon β I.Λ m)⁻¹) fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s t x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) ≤ ENNReal.ofReal 40

  c.flowreg display e.Xm.bound.2.

• composed_jacobian_smooth (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s t x

  Smooth spatial representative used to evaluate the essential-supremum seminorm bounds pointwise. This is qualitative flow regularity from §2.

• flow_jacobian (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ∀ (n : ℕ), 1 ≤ n → flowJacobianBarNorm n (2 ^ 14 * (epsilon β I.Λ m)⁻¹) (constructionFlowJacobian hseq m t s) ≤ ENNReal.ofReal 12

  c.flowreg display e.Xm.bound.3.

• flow_higher_derivative (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ∀ (n : ℕ), 1 ≤ n → ∀ (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => constructionFlow hseq m (s + t) y s) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ 2 * ↑n.factorial * (2 ^ 14 * (epsilon β I.Λ m)⁻¹) ^ (n - 1)

  Corrected c.flowreg derivative bound. The printed radius coefficient 2^13 fails at order seven (checked against the source); Scalars.flow_derivative_bound proves the corresponding conversion with 2^14.

• material_jacobian (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ∀ (n ell : ℕ), n + ell ≤ Nstar β → ∀ (i j : Fin 2) (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => constructionMaterialIterate (fun (r : ℝ) (z : Homogenization.Vec 2) => streamVel (Φ m) (s + r) z) ell (fun (r : ℝ) (z : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s r z) (Homogenization.basisVec j) i) t y) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ Cmat * (epsilon β I.Λ m)⁻¹ ^ n * (epsilon β I.Λ m ^ (β - 2)) ^ ell

  c.material.DX.Xinv, in its pointwise derivative form.

• material_jacobian_time_diff (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ), |t| ≤ 2 ^ (-25) * (AVenhance.a β I.Λ m)⁻¹ → ∀ (i j : Fin 2) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (r : ℝ) => (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec j) i) t

  Classical differentiability in target time of the entries appearing in c.material.DX.Xinv; this is the regularity implicit in that display's partial-time derivatives.

• inverse_jacobian_time_diff (m : ℕ) : 1 ≤ m → ∀ (s t : ℝ) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (r : ℝ) => constructionFlowInvJacobian hseq m r s x) t

  Classical target-time differentiability of the spatial inverse-flow Jacobian. This is the mixed regularity needed when differentiating the inverse transport equation in space.

• inverse_transport (m : ℕ) : 1 ≤ m → ∀ (t s : ℝ) (x : Homogenization.Vec 2), HasDerivAt (fun (r : ℝ) => constructionFlowInv hseq m r x s) (-(constructionFlowInvJacobian hseq m (t - s) s x) (streamVel (Φ m) t x)) t

  e.PDE.backwards for each stream flow.

theorem AVenhance.hasDerivAt_profile_spatialDerivative {t : ℝ} {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {Y : ℝ → Homogenization.Vec 2} {DY : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {Ydot : Homogenization.Vec 2} {DYdot : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hY : HasDerivAt Y Ydot t) (hDY : ∀ (v : Homogenization.Vec 2), HasDerivAt (fun (r : ℝ) => (DY r) v) (DYdot v) t) (v : Homogenization.Vec 2) : HasDerivAt (fun (r : ℝ) => (fderiv ℝ ψ (Y r)) ((DY r) v)) (((fderiv ℝ (fderiv ℝ ψ) (Y t)) Ydot) ((DY t) v) + (fderiv ℝ ψ (Y t)) (DYdot v)) t

Differentiate a transported spatial profile derivative when both the inverse trajectory and its spatial Jacobian have target-time derivatives.

theorem AVenhance.hasDerivAt_cutoff_mul_profile_spatialDerivative {t : ℝ} {c : ℝ → ℝ} {c' : ℝ} (hc : HasDerivAt c c' t) {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {Y : ℝ → Homogenization.Vec 2} {DY : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {Ydot : Homogenization.Vec 2} {DYdot : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hY : HasDerivAt Y Ydot t) (hDY : ∀ (v : Homogenization.Vec 2), HasDerivAt (fun (r : ℝ) => (DY r) v) (DYdot v) t) (v : Homogenization.Vec 2) : HasDerivAt (fun (r : ℝ) => c r * (fderiv ℝ ψ (Y r)) ((DY r) v)) (c' * (fderiv ℝ ψ (Y t)) ((DY t) v) + c t * (((fderiv ℝ (fderiv ℝ ψ) (Y t)) Ydot) ((DY t) v) + (fderiv ℝ ψ (Y t)) (DYdot v))) t

Product rule for the time-dependent cutoff multiplying a transported spatial profile derivative.

theorem AVenhance.norm_sub_le_of_uniform_deriv_le {f : ℝ → Homogenization.Vec 2} {B : ℝ} (hf : ∀ (t : ℝ), DifferentiableAt ℝ f t) (hderiv : ∀ (t : ℝ), ‖deriv f t‖ ≤ B) (s t : ℝ) : ‖f s - f t‖ ≤ B * |s - t|

The normed-vector mean-value estimate used to turn the differentiated recursion into a time-increment bound.

theorem AVenhance.continuous_norm_le_of_ae_le {f : Homogenization.Vec 2 → ℝ} {B : ℝ} (hf : Continuous f) (hB : 0 ≤ B) (h : ∀ᵐ (x : Homogenization.Vec 2), ‖f x‖ₑ ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖f x‖ ≤ B

theorem AVenhance.barNorm_iterated_pointwise {n : ℕ} {R B : ℝ} {f : Homogenization.Vec 2 → ℝ} (i : Fin n → Fin 2) (hf : Continuous fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)) (hR : 0 < R) (hB : 0 ≤ B) (h : barNorm n R f ≤ ENNReal.ofReal B) (x : Homogenization.Vec 2) : ‖(iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)‖ ≤ B / ((↑n + 1) ^ 2 / ↑n.factorial * R⁻¹ ^ n)

theorem AVenhance.continuous_iteratedCoordinate {n : ℕ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin n → Fin 2) : Continuous fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)

theorem AVenhance.composed_jacobian_spatial_partial_bound {β Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (hflow : FlowBoundsData I Φ hseq Cmat) {m : ℕ} (hm : 1 ≤ m) (s t : ℝ) (ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (i j k : Fin 2) (x : Homogenization.Vec 2) : ‖(fderiv ℝ (fun (y : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s t y) (Homogenization.basisVec j) i) x) (Homogenization.basisVec k)‖ ≤ 2 ^ 14 * (epsilon β I.Λ m)⁻¹

theorem AVenhance.q_minus_time_exponent_pos {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 0 < q β - (2 - β + 4 * delta β)

The exponent in the source comparison of the fast spatial and slow time scales is positive.

theorem AVenhance.epsilon_div_tau_le_constant {β : ℝ} {I : Ingredients β} (m : ℕ) (hm : 1 ≤ m) : epsilon β I.Λ m / tau β I.Λ m ≤ 2 ^ 33 * (1 + Infra.Ingredients.supergeoConstant β)

theorem AVenhance.tau_le_tauP {β : ℝ} {I : Ingredients β} (m : ℕ) (hm : 1 ≤ m) : tau β I.Λ m ≤ tauP β I.Λ m

def AVenhance.timeIncrementRotate (L : Homogenization.Vec 2 →L[ℝ] ℝ) : Homogenization.Vec 2

Rotate a spatial differential to form the velocity of a time increment.

Equations

• AVenhance.timeIncrementRotate L i = if i = 0 then -L (Homogenization.basisVec 1) else L (Homogenization.basisVec 0)

theorem AVenhance.timeIncrementRotate_zero : timeIncrementRotate 0 = 0

theorem AVenhance.timeIncrement_vec_decomp (v : Homogenization.Vec 2) : v = v 0 • Homogenization.basisVec 0 + v 1 • Homogenization.basisVec 1

theorem AVenhance.timeIncrement_vec_norm_le_coords (v : Homogenization.Vec 2) : ‖v‖ ≤ |v 0| + |v 1|

theorem AVenhance.streamVel_eq_timeIncrementRotate (φ : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : streamVel φ t x = timeIncrementRotate (fderiv ℝ (φ t) x)

theorem AVenhance.timeIncrementRotate_norm_le (L : Homogenization.Vec 2 →L[ℝ] ℝ) : ‖timeIncrementRotate L‖ ≤ 2 * ‖L‖

theorem AVenhance.timeIncrement_clm_norm_le_two_basis {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {L : Homogenization.Vec 2 →L[ℝ] F} {B : ℝ} (hB : 0 ≤ B) (h0 : ‖L (Homogenization.basisVec 0)‖ ≤ B) (h1 : ‖L (Homogenization.basisVec 1)‖ ≤ B) : ‖L‖ ≤ 2 * B

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

theorem AVenhance.stream_member_velocity_bound {β C : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : ‖streamVel (Φ m) t x‖ ≤ 2 * (|C| + 1) ^ 2

theorem AVenhance.psi_timeIncrement_contDiff {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (psi β I.Λ m k)

theorem AVenhance.psi_first_partial_timeIncrement_le {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) (i : Fin 2) (x : Homogenization.Vec 2) : ‖(fderiv ℝ (psi β I.Λ m k) x) (Homogenization.basisVec i)‖ ≤ 10 * a β I.Λ m * epsilon β I.Λ m

theorem AVenhance.psi_second_partial_timeIncrement_le {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) (J : Fin 2 → Fin 2) (x : Homogenization.Vec 2) : ‖(iteratedFDeriv ℝ 2 (psi β I.Λ m k) x) fun (j : Fin 2) => Homogenization.basisVec (J j)‖ ≤ 72 * a β I.Λ m

theorem AVenhance.psi_hessian_apply_timeIncrement_le {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) (y u v : Homogenization.Vec 2) : |((fderiv ℝ (fderiv ℝ (psi β I.Λ m k)) y) u) v| ≤ 4 * (72 * a β I.Λ m) * ‖u‖ * ‖v‖

theorem AVenhance.composed_flow_jacobian_entry_time_deriv_bound {β C Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (hflow : FlowBoundsData I Φ hseq Cmat) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (s t : ℝ) (ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (i j : Fin 2) (x : Homogenization.Vec 2) : |deriv (fun (r : ℝ) => (constructionComposedFlowJacobian hseq m s r x) (Homogenization.basisVec j) i) t| ≤ Cmat * epsilon β I.Λ m ^ (β - 2) + 2 ^ 15 * (epsilon β I.Λ m)⁻¹ * (2 * (|C| + 1) ^ 2)

theorem AVenhance.inverse_column_time_derivative_bound {K : ℝ} (t : ℝ) (G D : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (gdot ddot : Fin 2 → Homogenization.Vec 2) (hK : 0 ≤ K) (hGclose : ‖G t - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)‖ ≤ 1 / 4) (hDnorm : ‖D t‖ ≤ 2) (hcomp : ∀ (r : ℝ), G r ∘SL D r = ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) (hGdiff : ∀ (j : Fin 2), HasDerivAt (fun (r : ℝ) => (G r) (Homogenization.basisVec j)) (gdot j) t) (hDdiff : ∀ (j : Fin 2), HasDerivAt (fun (r : ℝ) => (D r) (Homogenization.basisVec j)) (ddot j) t) (hGdot : ∀ (j : Fin 2), ‖gdot j‖ ≤ K) (j : Fin 2) : ‖ddot j‖ ≤ 8 * K

theorem AVenhance.constructionFlowInvJacobian_entry_continuous {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (s t : ℝ) (i j : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => (constructionFlowInvJacobian hseq m t s x) (Homogenization.basisVec j) i

theorem AVenhance.inverse_flowJacobian_column_bound {β Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (hflow : FlowBoundsData I Φ hseq Cmat) (m : ℕ) (hm : 1 ≤ m) (s t : ℝ) (ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (x : Homogenization.Vec 2) : ‖constructionFlowInvJacobian hseq m t s x‖ ≤ 2

theorem AVenhance.inverseFlowJacobian_column_time_deriv_bound {β C Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (hflow : FlowBoundsData I Φ hseq Cmat) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (s t : ℝ) (ht : |t| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (x : Homogenization.Vec 2) (j : Fin 2) : ‖deriv (fun (r : ℝ) => (constructionFlowInvJacobian hseq m r s x) (Homogenization.basisVec j)) t‖ ≤ 16 * (Cmat * epsilon β I.Λ m ^ (β - 2) + 2 ^ 15 * (epsilon β I.Λ m)⁻¹ * (2 * (|C| + 1) ^ 2))