Flow derivative bounds for the composed-analyticity bridge

The stream-function higher-derivative field is the corrected e.Xm.bound.4 estimate in coordinate directions. This module converts it to the derivative seminorm used by AnalyticBridge.FlowForErgodicBound, and proves its support-time hypothesis from the cutoffs and time scales.

theorem AVenhance.Infra.Section5.AnalyticBridge.FlowForErgodicBound.orderedPartial_eq_iteratedFDeriv {n : ℕ} {f : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) : FaaDiBruno.orderedPartial n f x J = (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (J j)

theorem AVenhance.Infra.Section5.AnalyticBridge.FlowForErgodicBound.xiMK_ne_zero_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) {k : ℤ} {t : ℝ} (hne : I.xiMK m k t ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 5 / 4 * tau β I.Λ m

theorem AVenhance.Infra.Section5.AnalyticBridge.xFlow_derivativeSup_eXm_bound_four {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {R M : ℕ → ℝ} (hscales : Construction.Section2Scales I R M) (happB2 : Construction.AppB2InverseFlowData I Φ hΦ R M) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) (hprev : Construction.Section2StreamInductionHypothesis R M (m - 2)) {t : ℝ} (ht : |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹) (n : ℕ) : 1 ≤ n → FaaDiBruno.derivativeSup n (I.xFlow hΦ m (lIdx β I.Λ m k) t) ≤ ENNReal.ofReal (2 * ↑n.factorial * (2 ^ 14 * (epsilon β I.Λ (m - 1))⁻¹) ^ (n - 1))

Coordinate form of the corrected e.Xm.bound.4, obtained directly from the stream-function all-order field at the preceding scale. The radius coefficient is 2^14, as required by the source.

theorem AVenhance.Infra.Section5.AnalyticBridge.FlowForErgodicBound.xi_flow_time_window {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) : |t - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ 2 ^ (-25) * (a β I.Λ (m - 1))⁻¹

theorem AVenhance.Infra.Section5.AnalyticBridge.flowForErgodicBound_of_section2_previous {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {R M : ℕ → ℝ} (hscales : Construction.Section2Scales I R M) (happB2 : Construction.AppB2InverseFlowData I Φ hΦ R M) (m : ℕ) (hm : 2 ≤ m) (k : ℤ) (A : ℝ) (hA : 2 ^ 14 ≤ A) (hprev : Construction.Section2StreamInductionHypothesis R M (m - 2)) (t : ℝ) : t ∈ Set.Ioo 0 1 → I.xiMK m k t ≠ 0 → ∀ (n : ℕ), 1 ≤ n → FaaDiBruno.derivativeSup n (I.xFlow hΦ m (lIdx β I.Λ m k) t) ≤ ENNReal.ofReal (A * ↑n.factorial * (A / epsilon β I.Λ (m - 1)) ^ (n - 1))

The exact unfolded FlowForErgodicBound target on the support of ξ_{m,k}. Taking A ≥ 2^14 lets the stream-function coefficient 2 · (2^14)^(n-1) be absorbed into the source form A · A^(n-1).

theorem AVenhance.Infra.Section5.AnalyticBridge.flowForErgodicBound_of_appB2 {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {R M : ℕ → ℝ} (hscales : Construction.Section2Scales I R M) (happB2 : Construction.AppB2InverseFlowData I Φ hΦ R M) (A : ℝ) (hA : 2 ^ 14 ≤ A) (m : ℕ) : 2 ≤ m → ∀ t ∈ Set.Ioo 0 1, ∀ (k : ℤ), Odd k → I.xiMK m k t ≠ 0 → ∀ (n : ℕ), 1 ≤ n → FaaDiBruno.derivativeSup n (I.xFlow hΦ m (lIdx β I.Λ m k) t) ≤ ENNReal.ofReal (A * ↑n.factorial * (A / epsilon β I.Λ (m - 1)) ^ (n - 1))

Produce the exact unfolded hFlow family from the stream-function all-order AppB2 input. The previous-scale e.indyhyp is obtained by the proved Section 2 stream induction, so callers supply only the canonical scale and AppB2 data. The conclusion is definitionally equal to the FlowForErgodicBound predicate at each supported time.

theorem AVenhance.Infra.Section5.AnalyticBridge.flowForErgodicBound_of_stream {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (A : ℝ) (hA : 2 ^ 14 ≤ A) (m : ℕ) : 2 ≤ m → ∀ t ∈ Set.Ioo 0 1, ∀ (k : ℤ), Odd k → I.xiMK m k t ≠ 0 → ∀ (n : ℕ), 1 ≤ n → FaaDiBruno.derivativeSup n (I.xFlow hΦ m (lIdx β I.Λ m k) t) ≤ ENNReal.ofReal (A * ↑n.factorial * (A / epsilon β I.Λ (m - 1)) ^ (n - 1))

Instantiate the exact unfolded hFlow family from the canonical Section 2 scales and the smooth-flow AppB2 constructor. This is the form available directly from the stream-function stream witness.