CubeScaling

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

General-cube scaling of the coarse gauge

Source: ABK26, the deep-cube verification step of l.J.sensitivity.no.conditions. The unconditional sensitivity estimate applies the conditional per-cube machinery at a mesoscopic triadic cube R rather than at the unit cube. Two purely structural facts about a general triadic cube are needed for that.

• Descendant scaling of the gauge. On every triadic descendant S of a cube Q, the scale-normalized coarse gauge is monotone:

  |S| lambda_{s,q}^{-1}(S; A)  <=  |Q| lambda_{s,q}^{-1}(Q; A)   (2 s <= 1) ,
  

  where |Q| = cubeScaleFactor Q = 3^{Q.scale}. This is Book.Ch02.maxDescendant_lambdaSq_inv_le (CoarseGraining's form of e.bound.one.cube.by.lambdas) combined with the elementary exponent arithmetic l + 2 s (Q.scale - l) <= Q.scale.

• Well-definedness of lambda_{s,q}^{-1}(S; .). Two CoarseGraining triadic families whose representatives agree a.e. on a cube Q give the same value of lambda_{s,q}(S; .) at every S contained in Q. This is what lets the mesoscopic-cube gauge along the perturbation path be defined by a single concrete family (Provider.Lambda.CrudeBound.rootCoeffFamily) and still be computed by any compatible family.

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

Elementary facts about triadic cubes

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.le_finsetSupReal_of_mem {α : Type u_1} (s : Finset α) (f : α → ℝ) {R : α} (hR : R ∈ s) : f R ≤ HCPolySupport.Book.Ch02.finsetSupReal s f

A member of a finite family is bounded by its real supremum.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeScaleFactor_eq_rpow {d : ℕ} (R : HCPolySupport.TriadicCube d) : HCPolySupport.cubeScaleFactor R = Real.rpow 3 ↑R.scale

The cube scale factor as an rpow.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeScaleFactor_le_one_of_scale_nonpos {d : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R.scale ≤ 0) : HCPolySupport.cubeScaleFactor R ≤ 1

A cube of nonpositive scale has diameter at most one.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.mem_descendantsAtScale_self {d : ℕ} (R : HCPolySupport.TriadicCube d) : R ∈ HCPolySupport.descendantsAtScale R R.scale

Every cube is its own descendant at its own scale.

Descendant scaling of the coarse gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeScaleFactor_mul_multiscaleDescendantWeight_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs1 : 2 * s ≤ 1) {l : ℤ} (hl : l ≤ Q.scale) {S : HCPolySupport.TriadicCube d} (hS : S ∈ HCPolySupport.descendantsAtScale Q l) : HCPolySupport.cubeScaleFactor S * HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q l s ≤ HCPolySupport.cubeScaleFactor Q

The scale-weight bookkeeping of the descendant gauge scaling: 3^{l} 3^{2 s (Q.scale - l)} <= 3^{Q.scale} when 2 s <= 1 and l <= Q.scale.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeScaleFactor_mul_lambdaSq_inv_le_of_mem_descendantsAtScale {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs0 : 0 < s) (hs1 : 2 * s ≤ 1) (hq : q.IsAdmissible) {l : ℤ} (hl : l ≤ Q.scale) {S : HCPolySupport.TriadicCube d} (hS : S ∈ HCPolySupport.descendantsAtScale Q l) : HCPolySupport.cubeScaleFactor S * (HCPolySupport.Book.Ch02.lambdaSq S s q A)⁻¹ ≤ HCPolySupport.cubeScaleFactor Q * (HCPolySupport.Book.Ch02.lambdaSq Q s q A)⁻¹

Descendant scaling of the coarse gauge at a general cube. For every exponent pair with 2 s <= 1, the scale-normalized coarse gauge of a triadic descendant is bounded by that of its ancestor.

Well-definedness of the cube gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.coeffOn_aeeq_of_openCubeSet_subset {d : ℕ} {Q S : HCPolySupport.TriadicCube d} (hsub : HCPolySupport.openCubeSet S ⊆ HCPolySupport.openCubeSet Q) (A B : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hAB : (A.coeffOn Q).AEEq (B.coeffOn Q)) : (A.coeffOn S).AEEq (B.coeffOn S)

Two families that agree a.e. on a cube agree a.e. on every sub-cube.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.coarseSigmaStarInvMatrixNorm_eq_of_aeeq_of_openCubeSet_subset {d : ℕ} {Q S : HCPolySupport.TriadicCube d} (hsub : HCPolySupport.openCubeSet S ⊆ HCPolySupport.openCubeSet Q) (A B : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hAB : (A.coeffOn Q).AEEq (B.coeffOn Q)) : HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm S A = HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm S B

The one-cube observable |sigma_*^{-1}| only sees the a.e. class.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.lambdaSq_inv_eq_of_aeeq_of_openCubeSet_subset {d : ℕ} [NeZero d] {Q S : HCPolySupport.TriadicCube d} (hsub : HCPolySupport.openCubeSet S ⊆ HCPolySupport.openCubeSet Q) (A B : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hAB : (A.coeffOn Q).AEEq (B.coeffOn Q)) {s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (hs : 0 < s) (hq : q.IsAdmissible) : (HCPolySupport.Book.Ch02.lambdaSq S s q A)⁻¹ = (HCPolySupport.Book.Ch02.lambdaSq S s q B)⁻¹

Well-definedness of the cube gauge. If two CoarseGraining triadic families have a.e. equal representatives on a cube Q, then they give the same coarse gauge at every triadic cube contained in Q.