MesoscaleArithmetic

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The real arithmetic of the unconditional response aggregation

Source: ABK26.

This module contains the gauge-free real arithmetic of the aggregation half of l.J.sensitivity.no.conditions: the mesoscale exponent bookkeeping, the damping identities of the mesoscopic depth, and the single arithmetic fold that turns the four aggregated families into the four terms of the frozen conclusion Algsuperdiff.Frozen.Section24.responseJ_sensitivity_unconditional.

Nothing here mentions a coefficient field, a cube, a gauge or a multiscale quantity: every statement is about plain real numbers. It is split off from Provider.ResponseUnconditional.Aggregation purely so that each declaration elaborates inside the default heartbeat budget.

Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers.

Removing the mesoscale constant from the frozen rpow base

The mesoscopic depth is attached to u = 1 + C₀ X, while the frozen conclusion carries the bare base 1 + X. For C₀ ≥ 1 and an exponent in [0,1] the two differ by the harmless factor C₀.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.rpow_one_add_const_mul_le {C X θ : ℝ} (hC : 1 ≤ C) (hX : 0 ≤ X) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1) : (1 + C * X).rpow θ ≤ C * (1 + X).rpow θ

(1 +)^θ ≤ C (1 + X)^θ for 1 ≤ C, 0 ≤ X and 0 ≤ θ ≤ 1.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.frozen_exponent_mem {s t : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (ht0 : 0 ≤ t) (ht : t ≤ 1 / 4) : 0 ≤ 2 * t / (1 - 2 * s) ∧ 2 * t / (1 - 2 * s) ≤ 1

The frozen exponents 2t/(1-2s) lie in [0,1] on the frozen range 0 < s ≤ 1/4, 0 ≤ t ≤ 1/4.

The mesoscale rescaling factor against the frozen base

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.three_rpow_two_mul_depth_le_const_mul_rpow {s t X C₀ : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (ht0 : 0 ≤ t) (ht : t ≤ 1 / 4) (hX : 0 ≤ X) (hC₀ : 1 ≤ C₀) : Real.rpow 3 (2 * t * ↑(Mesoscale.mesoscaleDepth s (1 + C₀ * X))) ≤ 3 * C₀ * (1 + X).rpow (2 * t / (1 - 2 * s))

The mesoscale factor against the frozen rpow base. At the mesoscopic depth H = mesoscaleDepth s (1 + C₀ X), the descendant rescaling factor 3^{2 t H} is bounded by 3 C₀ (1 + X)^{2t/(1-2s)} — the frozen base carries no constant.

The damping identities of the mesoscopic depth

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.three_rpow_neg_two_one_sub_two_mul_le_one {s : ℝ} (hs : s ≤ 1 / 4) (H : ℕ) : Real.rpow 3 (-(2 * ((1 - 2 * s) * ↑H))) ≤ 1

The mesoscopic damping factor 3^{-2(1-2s)H} is at most one.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.three_rpow_neg_two_mul_rpow_le {s : ℝ} (hs0 : 0 ≤ s) (H : ℕ) : Real.rpow 3 (-(2 * ↑H)) * Real.rpow 3 (2 * s * ↑H) ≤ Real.rpow 3 (-(2 * ((1 - 2 * s) * ↑H)))

3^{-2H} · 3^{2sH} = 3^{-2(1-s)H} ≤ 3^{-2(1-2s)H}.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.three_rpow_neg_two_mul_rpow_sq_eq {s : ℝ} (H : ℕ) : Real.rpow 3 (-(2 * ↑H)) * Real.rpow 3 (2 * s * ↑H) ^ 2 = Real.rpow 3 (-(2 * ((1 - 2 * s) * ↑H)))

3^{-2H} · (3^{2sH})² = 3^{-2(1-2s)H}.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.sq_mul_damping_le_min {s X C₀ : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hX : 0 ≤ X) (hC₀ : 1 ≤ C₀) : X ^ 2 * Real.rpow 3 (-(2 * ((1 - 2 * s) * ↑(Mesoscale.mesoscaleDepth s (1 + C₀ * X))))) ≤ (C₀ ^ 2)⁻¹ * (max 1 (C₀ ^ 2) * min 1 X ^ 2)

The min bookkeeping of the fourth frozen term. At the mesoscopic depth attached to 1 + C₀ X the damped square X² 3^{-2(1-2s)H} is bounded by a constant multiple of min {1, X}².

The aggregation constant

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.aggConst (C₀ K : ℝ) : ℝ

The constant produced by the aggregation, in terms of the constant C₀ of the mesoscopic depth and the constant K of the per-cube estimate.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.aggConst C₀ K = 18 * C₀ + 3 * K * C₀ + K + 2 * K * max 1 (C₀ ^ 2) * (C₀ ^ 2)⁻¹

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.one_le_max_one_sq (C₀ : ℝ) : 1 ≤ max 1 (C₀ ^ 2)

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.aggConst_pos {C₀ K : ℝ} (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) : 0 < aggConst C₀ K

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.eighteen_mul_le_aggConst {C₀ K : ℝ} (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) : 18 * C₀ ≤ aggConst C₀ K

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.three_mul_le_aggConst {C₀ K : ℝ} (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) : 3 * K * C₀ ≤ aggConst C₀ K

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.le_aggConst {C₀ K : ℝ} (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) : K ≤ aggConst C₀ K

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.two_mul_min_coeff_le_aggConst {C₀ K : ℝ} (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) : 2 * (K * ((C₀ ^ 2)⁻¹ * max 1 (C₀ ^ 2))) ≤ aggConst C₀ K

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.min_coeff_le_aggConst {C₀ K : ℝ} (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) : K * ((C₀ ^ 2)⁻¹ * max 1 (C₀ ^ 2)) ≤ aggConst C₀ K

The arithmetic fold into the four frozen terms

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.main_term_le {μ C₀ K Wt Yt E : ℝ} (hμ : 0 < μ) (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) (hYt0 : 0 ≤ Yt) (hWt : Wt ≤ 3 * C₀ * Yt) : 6 * μ⁻¹ * (Wt * E ^ 2) ≤ aggConst C₀ K * μ⁻¹ * Yt * E ^ 2

The main term. 6 μ⁻¹ 3^{2tH} E² is one of the frozen first terms.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.value_term_le {μ σ0 C₀ K W Ys L val : ℝ} (hμ : 0 < μ) (hσ0 : 0 < σ0) (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) (hL : 0 ≤ L) (hYs0 : 0 ≤ Ys) (hW : W ≤ 3 * C₀ * Ys) : K * μ⁻¹ * σ0⁻¹ * (W * L) * val ^ 2 ≤ aggConst C₀ K * μ⁻¹ * σ0 * L * Ys * (σ0⁻¹ ^ 2 * val ^ 2)

The value term. K μ⁻¹ σ0⁻¹ 3^{2sH} λ⁻¹ ‖h‖²_{L²} is part of the second frozen term.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.shaking_term_le {μ σ0 C₀ K W Ys L : ℝ} (hμ : 0 < μ) (hσ0 : 0 < σ0) (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) (hL : 0 ≤ L) (hYs0 : 0 ≤ Ys) (hW : W ≤ 3 * C₀ * Ys) : K * μ⁻¹ * (μ - 1) ^ 2 * σ0 * (W * L) ≤ aggConst C₀ K * μ⁻¹ * σ0 * L * Ys * (μ - 1) ^ 2

The shaking term. K μ⁻¹ (μ-1)² σ0 3^{2sH} λ⁻¹ is the other part of the second frozen term.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.young_gradient_term_le {μ σ0 C₀ K W D2 Dm L gr : ℝ} (hμ : 0 < μ) (hσ0 : 0 < σ0) (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) (hW0 : 0 ≤ W) (hD20 : 0 ≤ D2) (hDm1 : Dm ≤ 1) (hD2W : D2 * W ≤ Dm) (hmin : (gr * L) ^ 2 * Dm ≤ (C₀ ^ 2)⁻¹ * (max 1 (C₀ ^ 2) * min 1 (gr * L) ^ 2)) : K * μ⁻¹ * σ0⁻¹ * (W * L) * (D2 * gr ^ 2) ≤ aggConst C₀ K * μ⁻¹ ^ 2 * σ0⁻¹ ^ 2 * gr ^ 2 + 2⁻¹ * aggConst C₀ K * min 1 (gr * L) ^ 2

The Young split of the mixed gradient term. The source's step in ABK26: μ⁻¹σ0⁻¹ λ⁻¹ ≤ ½(μ⁻²σ0⁻² + λ⁻²), after which the 3^{-2(1-s)H} damping sends the first half to the third frozen term and the second half to the fourth.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.pure_gradient_term_le {C₀ K W D2 Dm L gr : ℝ} (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) (hD2W2 : D2 * W ^ 2 = Dm) (hmin : (gr * L) ^ 2 * Dm ≤ (C₀ ^ 2)⁻¹ * (max 1 (C₀ ^ 2) * min 1 (gr * L) ^ 2)) : K * D2 * (W * L) ^ 2 * gr ^ 2 ≤ 2⁻¹ * aggConst C₀ K * min 1 (gr * L) ^ 2

The pure gradient term. K 3^{-2H} (3^{2sH} λ⁻¹)² ‖∇h‖² is the fourth frozen term.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.mesoscale_fold {μ σ0 C₀ K L gr val E Wt W D2 Dm Yt Ys : ℝ} (hμ : 0 < μ) (hσ0 : 0 < σ0) (hC₀ : 1 ≤ C₀) (hK : 0 ≤ K) (hL : 0 ≤ L) (hW0 : 0 ≤ W) (hD20 : 0 ≤ D2) (hYt0 : 0 ≤ Yt) (hYs0 : 0 ≤ Ys) (hWt : Wt ≤ 3 * C₀ * Yt) (hW : W ≤ 3 * C₀ * Ys) (hDm1 : Dm ≤ 1) (hD2W : D2 * W ≤ Dm) (hD2W2 : D2 * W ^ 2 = Dm) (hmin : (gr * L) ^ 2 * Dm ≤ (C₀ ^ 2)⁻¹ * (max 1 (C₀ ^ 2) * min 1 (gr * L) ^ 2)) : 6 * μ⁻¹ * (Wt * E ^ 2) + K * μ⁻¹ * σ0⁻¹ * (W * L) * val ^ 2 + (K * μ⁻¹ * (μ - 1) ^ 2 * σ0 * (W * L) + K * μ⁻¹ * σ0⁻¹ * (W * L) * (D2 * gr ^ 2) + K * D2 * (W * L) ^ 2 * gr ^ 2) ≤ aggConst C₀ K * μ⁻¹ * Yt * E ^ 2 + aggConst C₀ K * μ⁻¹ * σ0 * L * Ys * (σ0⁻¹ ^ 2 * val ^ 2 + (μ - 1) ^ 2) + aggConst C₀ K * μ⁻¹ ^ 2 * σ0⁻¹ ^ 2 * gr ^ 2 + aggConst C₀ K * min 1 (gr * L) ^ 2

The arithmetic fold of the aggregation. The four aggregated families are bounded by the four terms of the frozen conclusion.