Recursion

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Recursion.recursionCutoff {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ℝ → ℝ

Product cutoff localizing one term of the stream recursion in time.

Equations

• AVenhance.Recursion.recursionCutoff I m k t = I.hatZetaML m (AVenhance.lIdx β I.Λ m k) t * I.zetaMK m k t

theorem AVenhance.Recursion.recursionCutoff_contDiff {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (recursionCutoff I m k)

theorem AVenhance.Recursion.recursionCutoff_deriv_bound {β : ℝ} {I : Ingredients β} (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) : |deriv (recursionCutoff I m k) t| ≤ I.Czeta * I.Chat * ((tau β I.Λ m)⁻¹ + (tauP β I.Λ m)⁻¹)

theorem AVenhance.Recursion.zetaMK_ne_zero_distance {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) (t : ℝ) (hne : I.zetaMK m k t ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 2 / 3 * tau β I.Λ m

theorem AVenhance.Recursion.hatZetaML_ne_zero_distance {β : ℝ} {I : Ingredients β} {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (hne : I.hatZetaML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2

theorem AVenhance.Recursion.recursionCutoff_nonneg {β : ℝ} {I : Ingredients β} (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) : 0 ≤ recursionCutoff I m k t

theorem AVenhance.Recursion.recursionCutoff_deriv_zero_of_zero {β : ℝ} {I : Ingredients β} (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) (hz : recursionCutoff I m k t = 0) : deriv (recursionCutoff I m k) t = 0

theorem AVenhance.Recursion.epsilon_rpow_delta_le_one {β : ℝ} {I : Ingredients β} (m : ℕ) : epsilon β I.Λ m ^ delta β ≤ 1

theorem AVenhance.Recursion.epsilon_mul_previous_amplitude_le {β : ℝ} {I : Ingredients β} (m : ℕ) (hm : 1 ≤ m) : epsilon β I.Λ m * a β I.Λ (m - 1) ≤ 1 + Infra.Ingredients.supergeoConstant β

theorem AVenhance.Recursion.constructionFlow_zero {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) : constructionFlow hseq 0 = fun (x : ℝ) (x_1 : Homogenization.Vec 2) (x_2 : ℝ) => x_1

theorem AVenhance.Recursion.constructionFlowInv_zero {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) : constructionFlowInv hseq 0 = fun (x : ℝ) (x_1 : Homogenization.Vec 2) (x_2 : ℝ) => x_1

theorem AVenhance.Recursion.constructionFlowInvJacobian_zero {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (t s : ℝ) (x : Homogenization.Vec 2) : constructionFlowInvJacobian hseq 0 t s x = ContinuousLinearMap.id ℝ (Homogenization.Vec 2)

theorem AVenhance.Recursion.transported_profile_deriv_bound {β C Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (hflow : FlowBoundsData I Φ hseq Cmat) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) {c : ℝ → ℝ} {c' : ℝ} (hcdef : c = recursionCutoff I m k) {Y : ℝ → Homogenization.Vec 2} {D : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {Ydot : Homogenization.Vec 2} {Ddot : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (t : ℝ) (j : Fin 2) (hc : HasDerivAt c c' t) (hcval : c t ∈ Set.Icc 0 1) (hY : HasDerivAt Y Ydot t) (hD : ∀ (v : Homogenization.Vec 2), HasDerivAt (fun (r : ℝ) => (D r) v) (Ddot v) t) (hactive : c t ≠ 0 → ‖Ydot‖ ≤ 2 * (2 * (|C| + 1) ^ 2) ∧ ‖(D t) (Homogenization.basisVec j)‖ ≤ 2 ∧ ‖Ddot (Homogenization.basisVec j)‖ ≤ 16 * (Cmat * epsilon β I.Λ (m - 1) ^ (β - 2) + 2 ^ 15 * (epsilon β I.Λ (m - 1))⁻¹ * (2 * (|C| + 1) ^ 2))) : |deriv (fun (r : ℝ) => c r * (fderiv ℝ (psi β I.Λ m k) (Y r)) ((D r) (Homogenization.basisVec j))) t| ≤ (80 * I.Czeta * I.Chat * (2 ^ 33 * (1 + Infra.Ingredients.supergeoConstant β)) + 1152 * (2 * (|C| + 1) ^ 2) + 320 * Cmat * (1 + Infra.Ingredients.supergeoConstant β) + 320 * 2 ^ 15 * (2 * (|C| + 1) ^ 2)) * a β I.Λ m

theorem AVenhance.Recursion.nextStreamTerm_fderiv_formula {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (_hm : 1 ≤ m) (hφ : IsAdmissibleStream (Φ (m - 1))) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.nextStreamTerm m (Φ (m - 1)) hφ t y k) x ∧ (fderiv ℝ (fun (y : Homogenization.Vec 2) => I.nextStreamTerm m (Φ (m - 1)) hφ t y k) x) (Homogenization.basisVec j) = recursionCutoff I m k t * (fderiv ℝ (psi β I.Λ m k) (constructionFlowInv hseq (m - 1) t x (↑(lIdx β I.Λ m k) * tauPP β I.Λ m))) ((constructionFlowInvJacobian hseq (m - 1) (t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m) (↑(lIdx β I.Λ m k) * tauPP β I.Λ m) x) (Homogenization.basisVec j))

theorem AVenhance.Recursion.recursionCutoff_active_time_window {β : ℝ} {I : Ingredients β} (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) (hactive : recursionCutoff I m k t ≠ 0) : |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹

noncomputable def AVenhance.recursionProfileDerivativeConstant {β : ℝ} {I : Ingredients β} (C Cmat : ℝ) : ℝ

Constant controlling the spatial derivative of a recursive profile.

Equations

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

noncomputable def AVenhance.Recursion.recursionProfileSpatialDerivative {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (x : Homogenization.Vec 2) (j : Fin 2) : ℝ → ℝ

Cutoff-weighted spatial derivative of a single recursive profile.

Equations

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

theorem AVenhance.Recursion.recursion_profile_component_deriv_bound {β C Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (hreg : StreamRegularityBounds C I Φ) (hflow : FlowBoundsData I Φ hseq Cmat) (m : ℕ) (hm : 1 ≤ m) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : DifferentiableAt ℝ (recursionProfileSpatialDerivative hseq m k x j) t ∧ |deriv (recursionProfileSpatialDerivative hseq m k x j) t| ≤ recursionProfileDerivativeConstant C Cmat * a β I.Λ m

noncomputable def AVenhance.Recursion.recursionTermVelocity {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (_hseq : IsStreamSeq I Φ) (m : ℕ) (hφ : IsAdmissibleStream (Φ (m - 1))) (k : ℤ) (x : Homogenization.Vec 2) : ℝ → Homogenization.Vec 2

Velocity associated with one cutoff-weighted term of the stream recursion.

Equations

• AVenhance.Recursion.recursionTermVelocity _hseq m hφ k x r = AVenhance.timeIncrementRotate (fderiv ℝ (fun (y : Homogenization.Vec 2) => I.nextStreamTerm m (Φ (m - 1)) hφ r y k) x)

theorem AVenhance.Recursion.recursionTermVelocity_hasDeriv_bound {β C Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hflow : FlowBoundsData I Φ hseq Cmat) (m : ℕ) (hm : 1 ≤ m) (hφ : IsAdmissibleStream (Φ (m - 1))) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : HasDerivAt (recursionTermVelocity hseq m hφ k x) (deriv (recursionTermVelocity hseq m hφ k x) t) t ∧ ‖deriv (recursionTermVelocity hseq m hφ k x) t‖ ≤ 2 * recursionProfileDerivativeConstant C Cmat * a β I.Λ m

theorem AVenhance.Recursion.recursionCutoff_active_index {β : ℝ} {I : Ingredients β} (m : ℕ) (k : ℤ) (r t : ℝ) (hclose : |r - t| < tau β I.Λ m / 6) (hactive : recursionCutoff I m k r ≠ 0) : k ∈ Set.Icc ⌊t / tau β I.Λ m⌋ (⌊t / tau β I.Λ m⌋ + 1)

theorem AVenhance.Recursion.recursion_velocity_eq_pair_sum {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (hφ : IsAdmissibleStream (Φ (m - 1))) (hrec : Φ m = I.nextStream m (Φ (m - 1)) hφ) (t r : ℝ) (x : Homogenization.Vec 2) (hclose : |r - t| < tau β I.Λ m / 6) : streamVel (Φ m) r x - streamVel (Φ (m - 1)) r x = ∑ k ∈ {⌊t / tau β I.Λ m⌋, ⌊t / tau β I.Λ m⌋ + 1}, recursionTermVelocity hseq m hφ k x r

noncomputable def AVenhance.differentiatedRecursionTimeConstant {β : ℝ} (I : Ingredients β) (C Cmat : ℝ) : ℝ

The source-derived constant in the time increment estimate, assembled from the cutoff, inverse-flow, and material-Jacobian displays.

Equations

• AVenhance.differentiatedRecursionTimeConstant I C Cmat = 4 * AVenhance.recursionProfileDerivativeConstant C Cmat

theorem AVenhance.differentiated_recursion_time_increment_bound {β C Cmat : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hflow : FlowBoundsData I Φ hseq Cmat) : StreamVelocityTimeIncrementBound (differentiatedRecursionTimeConstant I C Cmat) I Φ

Differentiating the stream recursion on its two-index local overlap gives the time increment bound required by the limit-field regularity argument.

theorem AVenhance.limit_field_regular_of_stream_regularity {β C Cmat α : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hseq : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (hflow : FlowBoundsData I Φ hseq Cmat) (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 φ)

The packaged limit-field regularity conclusion follows from the stream-regularity spatial data and the explicit source-form flow/material bounds used to differentiate the stream recursion.