Material Flow Bounds

Support for the Armstrong–Vicol anomalous-diffusion formalization.

structure AVenhance.Infra.Construction.Section2SpatialFlowData {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hseq : IsStreamSeq I Φ) (m : ℕ) : Prop

The source-form §2 displays sufficient for the spatial slices of the material Jacobian consequences. This package deliberately excludes the material conclusion being derived below.

• flow_close (s r : ℝ) : |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (x : Homogenization.Vec 2), ‖constructionFlowJacobian hseq m r s x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)‖ ≤ 2 ^ 23 * |r| * AVenhance.a β I.Λ m ∧ 2 ^ 23 * |r| * AVenhance.a β I.Λ m ≤ 1 / 4
• flow_jacobian_composed (s r : ℝ) : |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ (n : ℕ), (flowJacobianBarNorm n (2 ^ 10 * (epsilon β I.Λ m)⁻¹) fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s r x - ContinuousLinearMap.id ℝ (Homogenization.Vec 2)) ≤ ENNReal.ofReal 40
• composed_jacobian_smooth (s r : ℝ) : |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => constructionComposedFlowJacobian hseq m s r x
• flow_higher_derivative (s r : ℝ) : |r| ≤ 2 ^ (-25) * (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 + r) y s) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ 2 * ↑n.factorial * (2 ^ 14 * (epsilon β I.Λ m)⁻¹) ^ (n - 1)

theorem AVenhance.Infra.Construction.MaterialFlowBounds.flow_slice_smooth {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => constructionFlow hseq m (s + r) y s

theorem AVenhance.Infra.Construction.MaterialFlowBounds.iteratedFDeriv_component {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Homogenization.Vec 2) (i : Fin 2) : (iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => f y i) x) J = (iteratedFDeriv ℝ n f x) J i

theorem AVenhance.Infra.Construction.MaterialFlowBounds.iteratedFDeriv_gradient_scalar {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (q : ℕ) (x : Homogenization.Vec 2) (J : Fin q → Fin 2) (j : Fin 2) : ((iteratedFDeriv ℝ q (fun (y : Homogenization.Vec 2) => (fderiv ℝ g y) (Homogenization.basisVec j)) x) fun (k : Fin q) => Homogenization.basisVec (J k)) = (iteratedFDeriv ℝ (q + 1) g x) (Fin.snoc (fun (k : Fin q) => Homogenization.basisVec (J k)) (Homogenization.basisVec j))

theorem AVenhance.Infra.Construction.MaterialFlowBounds.norm_iteratedFDeriv_neg {g : Homogenization.Vec 2 → ℝ} (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Homogenization.Vec 2) : ‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => -g y) x) J‖ = ‖(iteratedFDeriv ℝ n g x) J‖

theorem AVenhance.Infra.Construction.MaterialFlowBounds.fderiv_component_apply {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (i j : Fin 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => f y i) x) (Homogenization.basisVec j) = (fderiv ℝ f x) (Homogenization.basisVec j) i

theorem AVenhance.Infra.Construction.MaterialFlowBounds.fin_snoc_basisVec {n : ℕ} (J : Fin n → Fin 2) (j : Fin 2) : Fin.snoc (fun (k : Fin n) => Homogenization.basisVec (J k)) (Homogenization.basisVec j) = fun (k : Fin (n + 1)) => Homogenization.basisVec (Fin.snoc J j k)

theorem AVenhance.Infra.Construction.MaterialFlowBounds.basisVec_norm_eq_one (j : Fin 2) : ‖Homogenization.basisVec j‖ = 1

theorem AVenhance.Infra.Construction.MaterialFlowBounds.iteratedFDeriv_flowJacobian_entry {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) (i j : Fin 2) : ((iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => (constructionFlowJacobian hseq m r s y) (Homogenization.basisVec j) i) x) fun (k : Fin n) => Homogenization.basisVec (J k)) = (iteratedFDeriv ℝ (n + 1) (fun (y : Homogenization.Vec 2) => constructionFlow hseq m (s + r) y s) x) (Fin.snoc (fun (k : Fin n) => Homogenization.basisVec (J k)) (Homogenization.basisVec j)) i

theorem AVenhance.Infra.Construction.inverseJacobianPulledBack_cofactor_entries {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) (x : Homogenization.Vec 2) : (inverseJacobianPulledBack hseq m s r x) (Homogenization.basisVec 0) 0 = (constructionFlowJacobian hseq m r s x) (Homogenization.basisVec 1) 1 ∧ (inverseJacobianPulledBack hseq m s r x) (Homogenization.basisVec 1) 0 = -(constructionFlowJacobian hseq m r s x) (Homogenization.basisVec 1) 0 ∧ (inverseJacobianPulledBack hseq m s r x) (Homogenization.basisVec 0) 1 = -(constructionFlowJacobian hseq m r s x) (Homogenization.basisVec 0) 1 ∧ (inverseJacobianPulledBack hseq m s r x) (Homogenization.basisVec 1) 1 = (constructionFlowJacobian hseq m r s x) (Homogenization.basisVec 0) 0

theorem AVenhance.Infra.Construction.MaterialFlowBounds.pulledBackEntry_eq_flowJacobian_entry {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} (m : ℕ) (s r : ℝ) (i j : Fin 2) : (fun (x : Homogenization.Vec 2) => (inverseJacobianPulledBack hseq m s r x) (Homogenization.basisVec j) i) = if i = j then fun (x : Homogenization.Vec 2) => (constructionFlowJacobian hseq m r s x) (Homogenization.basisVec (1 - i)) (1 - j) else fun (x : Homogenization.Vec 2) => -(constructionFlowJacobian hseq m r s x) (Homogenization.basisVec (1 - i)) (1 - j)

theorem AVenhance.Infra.Construction.MaterialFlowBounds.flowJacobian_entry_norm_le_two {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {m : ℕ} (hflow : Section2SpatialFlowData I Φ hseq m) (s r : ℝ) (hr : |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹) (x : Homogenization.Vec 2) (i j : Fin 2) : ‖(constructionFlowJacobian hseq m r s x) (Homogenization.basisVec j) i‖ ≤ 2

theorem AVenhance.Infra.Construction.MaterialFlowBounds.iteratedFDeriv_add_const_eq_of_pos {n : ℕ} {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑n) f) (hn : 1 ≤ n) (c : ℝ) (x : Homogenization.Vec 2) (J : Fin n → Homogenization.Vec 2) : (iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => f y + c) x) J = (iteratedFDeriv ℝ n f x) J

def AVenhance.Infra.Construction.section2MaterialSpatialConstant (N : ℕ) : ℝ

The ell = 0 slice of c.material.DX.Xinv, derived from the explicit flow_jacobian_composed seminorm display in Section2FlowBoundsAtScale.

Equations

• AVenhance.Infra.Construction.section2MaterialSpatialConstant N = 42 + 40 * ∑ q ∈ Finset.range (N + 1), ↑q.factorial * 2 ^ (10 * q)

theorem AVenhance.Infra.Construction.section2_material_jacobian_spatial_slice_of_flow_bounds {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hseq : IsStreamSeq I Φ} {m N : ℕ} (hflow : Section2SpatialFlowData I Φ hseq m) : 1 ≤ section2MaterialSpatialConstant N ∧ ∀ (s r : ℝ), |r| ≤ 2 ^ (-25) * (a β I.Λ m)⁻¹ → ∀ n ≤ N, ∀ (i j : Fin 2) (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => (constructionComposedFlowJacobian hseq m s r y) (Homogenization.basisVec j) i) x) fun (k : Fin n) => Homogenization.basisVec (J k)‖ ≤ section2MaterialSpatialConstant N * (epsilon β I.Λ m)⁻¹ ^ n