CubeGauge

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

The coarse gauge of the perturbation path at a mesoscopic cube

Source: ABK26. The unconditional sensitivity estimate runs the conditional per-cube machinery on a mesoscopic triadic cube R of the unit-cube hierarchy rather than on the unit cube itself. The gauge that controls the machinery there is the R-local coarse gauge lambda_{3/8,2}^{-1}(R; a + tau h).

This module

• defines that gauge as a function of the path parameter, by evaluating Book.Ch02.lambdaSq at the concrete family Provider.Lambda.CrudeBound.rootCoeffFamily (so no choice is involved) and proves that any compatible family computes the same value (cubeGauge_eq_of_family, from lambdaSq_inv_eq_of_aeeq_of_openCubeSet_subset);
• records the crude uniform bound 4 d a.lam^{-1} valid along the whole segment, which the self-referential bootstrap of Provider.Lambda.Bootstrap consumes only through the choice of the compounding mesh;
• upgrades the pure-flux D_h bound of Provider.Lambda.CubeBound from the descendant gauge to the mesoscopic gauge, using the general-cube descendant scaling of CubeScaling; and
• assembles the resulting differential inequality into the ratio engine at R, exactly as Provider.Lambda.Engine does at the unit cube, but with the R-local gauge and the R-local constant.

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.isAdmissible_finite_two : (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2).IsAdmissible

The mesoscopic-cube gauge along the path

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeGauge {d : ℕ} (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (τ : ℝ) : ℝ

The mesoscopic-cube coarse gauge along the perturbation path. The R-local value of lambda_{3/8,2}^{-1} at the coefficient field a + tau h, evaluated at the concrete compatible family rootCoeffFamily.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeGauge_nonneg {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (τ : ℝ) : 0 ≤ cubeGauge R a h τ

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeGauge_eq_of_family {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (τ : ℝ) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hA : (A.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h τ)) : (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A)⁻¹ = cubeGauge R a h τ

Any compatible family computes the mesoscopic-cube gauge.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeGauge_zero_eq_of_family {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) : (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ = cubeGauge R a h 0

The base point of the path: any family compatible with a computes the mesoscopic-cube gauge at tau = 0.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeGauge_le_crude {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (τ : ℝ) : cubeGauge R a h τ ≤ 4 * ↑d * a.lam⁻¹

The crude uniform bound for the mesoscopic-cube gauge. The microscopic ellipticity constant of the base coefficient appears here and only here; the bootstrap consumes it through the compounding mesh only.

The mesoscopic-cube constant of the D_h bound

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.mesoFluxConst (d : ℕ) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) : ℝ

The constant of the pure-flux D_h bound at the mesoscopic cube R, in the normalization |D_h| <= 2 (K Psi) J used by the ratio engine.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.mesoFluxConst_nonneg (d : ℕ) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (R : HCPolySupport.TriadicCube d) : 0 ≤ mesoFluxConst d h R

The D_h bound with the mesoscopic gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.abs_dhFluxForm_le_cubeGauge {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {R : HCPolySupport.TriadicCube d} (hRscale : R.scale ≤ 0) {l : ℤ} (hlroot : l ≤ (HCPolySupport.originCube d 0).scale) {S : HCPolySupport.TriadicCube d} (hSroot : S ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) l) (hSR : S ∈ HCPolySupport.descendantsAtScale R l) (τ : ℝ) (w : HCPolySupport.Vec d) : |Lambda.dhFluxForm (HCPolySupport.Book.Ch02.cubeDomain S) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain S) (F.coeffOn S) (Lambda.descendantField hlroot hSroot h.toLInfSkewMatrixFieldOn) τ) (Lambda.descendantField hlroot hSroot h.toLInfSkewMatrixFieldOn) w| ≤ 2 * (mesoFluxConst d h R * cubeGauge R a h.toLInfSkewMatrixFieldOn τ) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain S) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain S) (F.coeffOn S) (Lambda.descendantField hlroot hSroot h.toLInfSkewMatrixFieldOn) τ) 0 w

The pure-flux D_h bound with the mesoscopic gauge. On every triadic descendant S of the mesoscopic cube R, and along the whole perturbation path, the pure-flux D_h form is controlled by the R-local coarse gauge.

The ratio engine at the mesoscopic cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.cubeGauge_ratio_engine {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (τ₁ τ₂ C : ℝ) (h12 : τ₁ ≤ τ₂) (hC : ∀ (τ : ℝ), τ₁ ≤ τ → τ ≤ τ₂ → cubeGauge R a h.toLInfSkewMatrixFieldOn τ ≤ C) : cubeGauge R a h.toLInfSkewMatrixFieldOn τ₂ ≤ Real.exp (mesoFluxConst d h R * C * (τ₂ - τ₁)) * cubeGauge R a h.toLInfSkewMatrixFieldOn τ₁

The ratio engine at the mesoscopic cube. Given a bound C for the R-local coarse gauge on a subinterval of the path, the gauge itself obeys the multiplicative Grönwall ratio on that subinterval. This is Provider.Lambda.Engine.pathLambdaInv_ratio_engine transplanted from the unit cube to the mesoscopic cube R.