The L²_x → L¹ composed-analyticity bridge (route A)

e.Tm.reg.upgrade (all orders, L²_x) + H² ⊂ L∞ + l.product + proposition 10528 + e.flow.for.ergodic give the averaged coordinate-derivative bounds for ∂_iT ∂_jT ∘ X required by l.flow.averages. The constant is A' ρ^{-6} ‖θ₀‖² with radius ρ / A'.

noncomputable def AVenhance.Infra.Section5.AnalyticBridge.bridgeConst (K A : ℝ) : ℝ

The bridge constant A' = 4 (3 sc K)² A⁸ + (2 + 8K) A².

Equations

• AVenhance.Infra.Section5.AnalyticBridge.bridgeConst K A = 4 * (3 * AVenhance.Infra.Section5.AnalyticBridge.sobolevConst * K) ^ 2 * A ^ 8 + (2 + 8 * K) * A ^ 2

theorem AVenhance.Infra.Section5.AnalyticBridge.one_le_bridgeConst {K A : ℝ} (hK : 1 ≤ K) (hA : 1 ≤ A) : 1 ≤ bridgeConst K A

theorem AVenhance.Infra.Section5.AnalyticBridge.radius_le_bridgeConst {K A ρ e : ℝ} (hK : 1 ≤ K) (hA : 1 ≤ A) (hρ : 0 < ρ) (hρe : ρ ≤ e) : 2 * A / e * (1 + ↑2 * (K * e) * (2 * (A / ρ))) ≤ bridgeConst K A / ρ

The composed radius is at most A' / ρ.

theorem AVenhance.Infra.Section5.AnalyticBridge.amplitude_le_bridgeConst {K A ρ N : ℝ} (hK : 1 ≤ K) (hA : 1 ≤ A) (hρ : 0 < ρ) : 4 * (3 * sobolevConst * (A * N) * K * (A / ρ) ^ 3) ^ 2 ≤ bridgeConst K A * ρ ^ (-6) * N ^ 2

The composed amplitude is at most A' ρ^{-6} N².

theorem AVenhance.Infra.Section5.AnalyticBridge.combine_bound {K A ρ N : ℝ} (hK : 1 ≤ K) (hA : 1 ≤ A) (hρ : 0 < ρ) {e : ℝ} (hρe : ρ ≤ e) (n : ℕ) : 4 * (3 * sobolevConst * (A * N) * K * (A / ρ) ^ 3) ^ 2 * ↑n.factorial * (2 * A / e * (1 + ↑2 * (K * e) * (2 * (A / ρ)))) ^ n ≤ bridgeConst K A * ρ ^ (-6) * N ^ 2 * ↑n.factorial / (ρ / bridgeConst K A) ^ n

Abstract-real combination of amplitude and radius bounds into the target shape.

Integration over the unit cell and the main theorem

theorem AVenhance.Infra.Section5.AnalyticBridge.volume_unitCell_le_one : MeasureTheory.volume (Torus.unitCell 2) ≤ 1

The half-open unit cell has volume at most one.

theorem AVenhance.Infra.Section5.AnalyticBridge.integral_norm_unitCell_le {g : Homogenization.Vec 2 → ℂ} {M : ℝ} (hM : 0 ≤ M) (h : ∀ (x : Homogenization.Vec 2), ‖g x‖ ≤ M) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, ‖g x‖ ≤ M

A pointwise bound gives the same bound for the unit-cell average of the norm.

theorem AVenhance.Infra.Section5.AnalyticBridge.nonneg_l2NormSq (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

theorem AVenhance.Infra.Section5.AnalyticBridge.fderiv_eq_zero_of_amplitude_zero {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {a : ℝ} (ha : 1 ≤ a) (hreg : ∀ (n : ℕ) (i : Fin n → Fin 2), √(l2NormSq fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)) ≤ 0 * ↑n.factorial * a ^ n) (v : Fin 2) (x : Homogenization.Vec 2) : (fderiv ℝ f x) (Homogenization.basisVec v) = 0

If θ₀ = 0 in L², the gradient of every admissible T(t) vanishes.

theorem AVenhance.Infra.Section5.AnalyticBridge.hasCoordinateAnalyticL1Bounds_of_bounds (A : ℝ) (hA : 1 ≤ A) : ∃ (A' : ℝ), 1 ≤ A' ∧ ∀ (θ₀ : Homogenization.Vec 2 → ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (ρ e : ℝ) (X : Homogenization.Vec 2 → Homogenization.Vec 2), 0 < ρ → ρ ≤ e → e ≤ 1 → TmRegUpgradeLinfL2 A ρ θ₀ T → FlowForErgodicBound A e X → ContDiff ℝ (↑⊤) X → ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (T t) → IsZ2Periodic (T t) → ∀ (i j : Fin 2), Ergodic.HasCoordinateAnalyticL1Bounds (fun (y : Homogenization.Vec 2) => ↑(spaceGrad (T t) (X y) i * spaceGrad (T t) (X y) j)) (A' * ρ ^ (-6) * l2NormSq θ₀) (ρ / A')

Route A bridge: e.Tm.reg.upgrade (all orders, L²_x), H² ⊂ L∞, l.product, proposition 10528 and e.flow.for.ergodic give the composed L¹ analyticity required by l.flow.averages. Amplitude A' ρ^{-6} ‖θ₀‖² (so p = 6), radius ρ / A'.