Source hypotheses of the L²_x → L¹ analyticity bridge

The two source estimates that feed the composed-analyticity bridge: the all-orders L∞_t L²_x part of e.Tm.reg.upgrade and the flow bound e.flow.for.ergodic.

def AVenhance.Infra.Section5.AnalyticBridge.TmRegUpgradeLinfL2 (A ρ : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) : Prop

e.Tm.reg.upgrade, the L∞_t L²_x part, for every order n (multi-index form, t ∈ [0,1]), with constant A and length scale ρ = e^{1+γ/2}.

Equations

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

def AVenhance.Infra.Section5.AnalyticBridge.FlowForErgodicBound (A e : ℝ) (X : Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

e.flow.for.ergodic (7066–7071) for one flow slice X, length scale e = ε_{m-1}.

Equations

• AVenhance.Infra.Section5.AnalyticBridge.FlowForErgodicBound A e X = ∀ (n : ℕ), 1 ≤ n → AVenhance.FaaDiBruno.derivativeSup n X ≤ ENNReal.ofReal (A * ↑n.factorial * (A / e) ^ (n - 1))