WitnessBudget

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

The pure-flux zero-trace witness budget at a general triadic cube

Source: ABK26 (e.split.besov.stuff.begin) specialized to the pure-flux loading p = 0 and stated at an arbitrary triadic cube.

At p = 0 the source combination degenerates:

∇u = ∇w + ∇w^* = ½ (∇v(·,Q,0,q;a) + ∇v(·,Q,0,-q;aᵗ)) ,

with no affine summand. Consequently the budget is a clean multiple of λ_{3/8,2}^{-1/2} J^{1/2} with no |p·q| term, and neither Discharge.ConstantBesov nor Discharge.EllipticityOrdered is needed.

Two general-cube inputs make this work at a descendant cube:

• the coarse Poincaré estimate of Assembly.GaugeBridge, which is already stated at an arbitrary triadic cube and an arbitrary CoarseGraining family;
• the transpose invariance of the multiscale gauge (Discharge.TransposeGauge.lambdaSq_transposeCoeffFamily) together with the pure-flux adjoint identity J(Q, aᵗ, 0, -q) = J(Q, a, 0, q), which at p = 0 carries no shift.

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

Measure bridges at a general triadic cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeDomain_coe_openCubeSet {d : ℕ} (Q : HCPolySupport.TriadicCube d) : (HCPolySupport.Book.Ch02.cubeDomain Q).carrier = HCPolySupport.openCubeSet Q

The Chapter 2 carrier of cubeDomain Q is the open cube.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.memLp_normalizedCubeMeasure_of_memLp_cubeDomain {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {r : ENNReal} {f : HCPolySupport.Vec d → E} (Q : HCPolySupport.TriadicCube d) (hf : MeasureTheory.MemLp f r (HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain Q).carrier)) : MeasureTheory.MemLp f r (HCPolySupport.normalizedCubeMeasure Q)

L^p membership on the open-cube carrier transfers to the normalized cube measure, at an arbitrary triadic cube.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.ae_normalizedCubeMeasure_of_ae_cubeDomain {d : ℕ} {P : HCPolySupport.Vec d → Prop} (Q : HCPolySupport.TriadicCube d) (h : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain Q).carrier, P x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure Q, P x

Any a.e. property on the open-cube carrier holds a.e. for the normalized cube measure, at an arbitrary triadic cube.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.ae_cubeDomain_iff_normalizedCubeMeasure {d : ℕ} {E : Type u_1} {f g : HCPolySupport.Vec d → E} (Q : HCPolySupport.TriadicCube d) (h : f =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain Q).carrier] g) : f =ᵐ[HCPolySupport.normalizedCubeMeasure Q] g

A.e. equality on the open-cube carrier transfers to the normalized cube measure, at an arbitrary triadic cube.

The two maximizer-gradient budgets at a general cube

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovNegativeVectorSeminormTwo_cubeMaximizerGrad_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch03.CoeffFamily d) {p q : HCPolySupport.Vec d} {v : HCPolySupport.Book.Ch03.CubeSolution Q F} (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p q v) : (HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q (3 / 8) fun (x : HCPolySupport.Vec d) => v.toH1.grad x) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * √(HCPolySupport.Book.Ch02.lambdaSq Q (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ * (2 * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p q))

The negative Besov budget of a response-maximizer gradient at an arbitrary triadic cube, in the concrete q = 2 spelling.

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovNegativeVectorSeminormTwo_cubeAdjointGrad_flux_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch03.CoeffFamily d) {w : HCPolySupport.Vec d} {vAdj : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q).transpose} (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q).transpose 0 (-w) vAdj) : (HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q (3 / 8) fun (x : HCPolySupport.Vec d) => vAdj.toH1.grad x) ≤ HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * √(HCPolySupport.Book.Ch02.lambdaSq Q (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ * (2 * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) 0 w))

The adjoint budget at the pure-flux loading. At p = 0 the transposed response equals the primal one, so there is no |p·q| shift.

The pure-flux witness-gradient budget

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxWitnessConst : ℝ

The explicit constant of the pure-flux witness-gradient negative Besov budget.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxWitnessConst = 2 * √2 * HCPolySupport.Book.Ch03.poincareDiscountFactor (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2)

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.fluxWitnessConst_nonneg : 0 ≤ fluxWitnessConst

theorem Algsuperdiff.Section24.Sensitivity.Provider.Lambda.cubeBesovNegativeVectorSeminormTwo_fluxWitnessGrad_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch03.CoeffFamily d) (w : HCPolySupport.Vec d) {vAdj : HCPolySupport.Book.Ch02.Solution (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q).transpose} {v : HCPolySupport.Book.Ch03.CubeSolution Q F} (hvAdj : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q).transpose 0 (-w) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) 0 w v) (u : HCPolySupport.H10Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (hu : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (HCPolySupport.Book.Ch02.cubeDomain Q).carrier, u.grad x = 2⁻¹ • (vAdj.toH1.grad x + v.toH1.grad x) + 0) : (HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x) ≤ fluxWitnessConst * (√(HCPolySupport.Book.Ch02.lambdaSq Q (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) F)⁻¹ * √(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) 0 w))

The pure-flux negative Besov budget of the zero-trace witness gradient at an arbitrary triadic cube.

At p = 0 there is no affine summand, so the budget is a pure multiple of λ_{3/8,2}^{-1/2} J^{1/2}.