CubeGaugePath

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

Descendant-gauge control along the perturbation path

Source: ABK26, the scaled-norm inequalities that precede the descendant b-matrix estimate.

The pure-potential D_h bound of BigLambda.CubePotentialDh prices its Term A against the descendant gauge λ_{3/8,2}^{-1}(R; a + τh), so the Young/Grönwall absorption at the cube R needs that gauge to stay comparable to its value at the base point τ = 0.

The proof does not rerun the lambda_{s,q} spine at R: it reuses the per-descendant pure-flux estimate Provider.Lambda.abs_dhFluxForm_le_root_gauge (which already prices everything against the root gauge), turns it into the per-cube response ratio with Provider.Lambda.Engine, converts that into the one-cube σ_*^{-1} ratio with Provider.Lambda.DescendantBridge, and finally aggregates at R with the general-cube Provider.Multiscale.lambdaSq_inv_le_of_descendant_ratio. The aggregation is legitimate because every descendant of R is a descendant of the unit cube (Homogenization.mem_descendantsAtScale_trans).

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

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.gaugeGateConst (d : ℕ) : ℝ

The flux-based threshold constant for the cube gauge estimate.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.gaugeGateConst d = 8 * Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxSpineConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.gaugeGateConst_pos (d : ℕ) : 0 < gaugeGateConst d

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.gate_mul_lambdaSq_inv_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (gaugeGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) : h.gradientW1Infinity * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ (8 * Lambda.fluxSpineConst d)⁻¹

The frozen gate in multiplicative form.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.dhFluxForm_root_gauge_bound {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F' : HCPolySupport.Book.Ch03.CoeffFamily d) : (F'.coeffOn (HCPolySupport.originCube d 0)).AEEq a → ∀ (l : ℤ) (hl : l ≤ (HCPolySupport.originCube d 0).scale) (T : HCPolySupport.TriadicCube d) (hT : T ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) l) (σ : ℝ) (w : HCPolySupport.Vec d), |Lambda.dhFluxForm (HCPolySupport.Book.Ch02.cubeDomain T) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain T) (F'.coeffOn T) (Lambda.descendantField hl hT h.toLInfSkewMatrixFieldOn) σ) (Lambda.descendantField hl hT h.toLInfSkewMatrixFieldOn) w| ≤ 2 * (Lambda.fluxSpineConst d * h.gradientW1Infinity * Lambda.pathGauge a h.toLInfSkewMatrixFieldOn σ) * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain T) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain T) (F'.coeffOn T) (Lambda.descendantField hl hT h.toLInfSkewMatrixFieldOn) σ) 0 w

The pure-flux descendant D_h bound in the exact shape consumed by the spine and by Provider.Response.PathGauge.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.four_mul_gate_le {d : ℕ} [NeZero d] (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (gaugeGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) : 4 * (Lambda.fluxSpineConst d * h.gradientW1Infinity) * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ 1 / 2

The smallness gate in the shape consumed by the spine.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.pathGauge_le_two_mul_of_gate {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (gaugeGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) {σ : ℝ} (hσ0 : 0 ≤ σ) (hσ1 : σ ≤ 1) : Lambda.pathGauge a h.toLInfSkewMatrixFieldOn σ ≤ 2 * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

The root gauge at most doubles along the path.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.cubeScaleFactor_le_one_of_mem_descendantsAtScale {d : ℕ} {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) : HCPolySupport.cubeScaleFactor R ≤ 1

Descendants of the unit cube have side length at most one.

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.lambdaSq_inv_perturb_cube_le_two_mul {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (hgate : h.gradientW1Infinity ≤ (gaugeGateConst d)⁻¹ * Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a) (F G : HCPolySupport.Book.Ch03.CoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {τ : ℝ} (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1) (hG : (G.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn τ)) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) : (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹ ≤ 2 * (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹

Descendant-gauge doubling along the path.

Under the frozen smallness gate, at every triadic descendant R of the unit cube the coarse gauge at the endpoint a + h is at most twice its value at the base point a.