ScaleSelection

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

The mesoscopic scale-selection arithmetic for the unconditional sensitivity estimates

The unconditional Section 2.4 sensitivity estimates (ABK26, Lemma l.J.sensitivity.no.conditions) remove the smallness assumption of the conditional estimates by choosing a mesoscopic scale 3^{-h} as a function of the dimensionless quantity X = ||grad h||_{W^{1,infinity}(cube_0)} * lambda_{s,2}^{-1}(cube_0; a),

applying the conditional estimates on every triadic cube of that scale, and reassembling. The source's choice is h := ceil ( (1 - 2 s)^{-1} log_3 u ), u = 1 + >= 1,

and the only property of h used afterwards is the two-sided bound e.another.way.to.say.h 3^{(1-2s) h - 1} <= u <= 3^{(1-2s) h}.

This module contains only that pure real-analysis arithmetic together with the exponent bookkeeping it feeds:

• mesoscaleDepth and the two-sided bound three_rpow_mesoscaleDepth_sub_one_le / le_three_rpow_mesoscaleDepth;
• three_rpow_two_mul_mesoscaleDepth_le — the conversion of the per-cube rescaling factor 3^{2 t h} into 3 * u^{2t/(1-2s)}, which is where the literal factor 3 of the frozen constant 6 = 2 * 3 and the exponent 2t/(1-2s) of lambda_sensitivity_unconditional come from (and, at t := s, the exponent 2s/(1-2s) of responseJ_sensitivity_unconditional);
• sub_one_mul_three_rpow_neg_mesoscaleDepth_le_one — the statement that the smallness condition of the conditional estimates does hold at the mesoscopic scale, in dimensionless form;
• sub_one_sq_mul_three_rpow_neg_two_mesoscaleDepth_le_min and min_one_sq_mul_le — the min {1, X}^2 bookkeeping of the fourth term of responseJ_sensitivity_unconditional;
• three_rpow_neg_two_mul_one_sub_le — the comparison 3^{-2(1-s)h} <= 3^{-2(1-2s)h} used by the Young-inequality step of the source.

Nothing here mentions a coefficient field, a cube, a gauge or a multiscale quantity: every statement is about plain real numbers. In particular this file is gauge-free and is shared by the lambda and the responseJ halves of the unconditional estimates.

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

The mesoscopic depth

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.mesoscaleDepth (s u : ℝ) : ℕ

The mesoscopic scale-separation parameter h of ABK26: the number of triadic scales one descends before applying the conditional sensitivity estimates. Here u stands for the source's 1 + C ||grad h||_{W^{1,infinity}} lambda_{s,2}^{-1}.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.mesoscaleDepth s u = ⌈Real.logb 3 u / (1 - 2 * s)⌉₊

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.le_three_rpow_mesoscaleDepth {s u : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) : u ≤ Real.rpow 3 ((1 - 2 * s) * ↑(mesoscaleDepth s u))

The upper half of e.another.way.to.say.h: u <= 3^{(1-2s) h}.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.three_rpow_mesoscaleDepth_sub_one_le {s u : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) : Real.rpow 3 ((1 - 2 * s) * ↑(mesoscaleDepth s u) - 1) ≤ u

The lower half of e.another.way.to.say.h: 3^{(1-2s) h - 1} <= u.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.three_rpow_mesoscaleDepth_le_three_mul {s u : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) : Real.rpow 3 ((1 - 2 * s) * ↑(mesoscaleDepth s u)) ≤ 3 * u

Restatement of the lower half of e.another.way.to.say.h: 3^{(1-2s) h} <= 3 u.

Exponent bookkeeping

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.three_rpow_two_mul_mesoscaleDepth_le_rpow {s u t : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) (ht : 0 ≤ t) : Real.rpow 3 (2 * t * ↑(mesoscaleDepth s u)) ≤ (3 * u).rpow (2 * t / (1 - 2 * s))

The per-cube rescaling factor 3^{2 t h} at the mesoscopic depth is bounded by (3 u)^{2t/(1-2s)}.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.three_rpow_two_mul_mesoscaleDepth_le {s u t : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) (ht : 0 ≤ t) (ht' : t ≤ 1 / 4) : Real.rpow 3 (2 * t * ↑(mesoscaleDepth s u)) ≤ 3 * u.rpow (2 * t / (1 - 2 * s))

The exponent bookkeeping of the unconditional estimates. For s, t in the frozen range (0, 1/4] the per-cube rescaling factor 3^{2 t h} at the mesoscopic depth is bounded by 3 * u^{2t/(1-2s)}.

Taken with t and the factor 2 coming from the conditional lambda sensitivity estimate at the mesoscopic cubes, this is the exact source of the literal constant 6 = 2 * 3 and of the exponent 2t/(1-2s) in lambda_sensitivity_unconditional; taken with t := s it is the source of the exponent 2s/(1-2s) in responseJ_sensitivity_unconditional.

The smallness condition at the mesoscopic scale

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.sub_one_mul_three_rpow_neg_mesoscaleDepth_le_one {s u : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) : (u - 1) * Real.rpow 3 (-((1 - 2 * s) * ↑(mesoscaleDepth s u))) ≤ 1

The smallness condition holds at the mesoscopic scale. In dimensionless form: the mesoscopic depth is chosen exactly so that (u - 1) 3^{-(1-2s) h} <= 1, where u - 1 stands for the source's C ||grad h||_{W^{1,infinity}(cube_0)} lambda_{s,2}^{-1}(cube_0; a).

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.sub_one_sq_mul_three_rpow_neg_two_mesoscaleDepth_le_one {s u : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) : (u - 1) ^ 2 * Real.rpow 3 (-(2 * ((1 - 2 * s) * ↑(mesoscaleDepth s u)))) ≤ 1

The squared form of the previous bound.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.sub_one_sq_mul_three_rpow_neg_two_mesoscaleDepth_le_min {s u : ℝ} (hs0 : 0 < s) (hs : s ≤ 1 / 4) (hu : 1 ≤ u) : (u - 1) ^ 2 * Real.rpow 3 (-(2 * ((1 - 2 * s) * ↑(mesoscaleDepth s u)))) ≤ min 1 ((u - 1) ^ 2)

The 3^{-2(1-2s)h}-damped square is bounded by min {1, (u-1)^2}.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Mesoscale.min_one_sq_mul_le (C X : ℝ) : min 1 ((C * X) ^ 2) ≤ max 1 (C ^ 2) * min 1 X ^ 2

Repackaging of the min bookkeeping: with u - 1 = C X and C, X >= 0, min {1,^2} is bounded by max {1, C^2} * min {1, X}^2. This is the step that turns the mesoscale bound into the fourth term C * min 1 (gradientW1Infinity * lambda_{s,2}^{-1}) ^ 2 of responseJ_sensitivity_unconditional.

The Young-inequality comparison of damping exponents

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

For 0 <= s and n : ℕ, 3^{-2(1-s)n} <= 3^{-2(1-2s)n}. This is the comparison used by the Young-inequality step of the source in ABK26, where the 3^{-2(1-s)h} damping of the gradient term is absorbed into the min {1, .}^2 term.