CubeWitnessPQ

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

The zero-trace witness budget at a general loading

Source: ABK26 (e.split.besov.stuff.begin), at the general loading (p, q) and at an arbitrary triadic cube R.

Provider.BigLambda.CubeWitness proves the same budget at the pure-potential loading q = 0, where the adjoint response coincides with the primal one and the loading term |p| is controlled by J(R,p,0) alone. At a general loading two changes occur, and neither is a specialization of the other:

• the adjoint maximizer solves the (p, -q) problem for aᵗ, and Provider.DhBound.Discharge.responseJ_transpose_neg_right gives J(R, aᵗ, p, -q) = J(R, a, p, q) + 2 p·q, i.e. an extra |p·q| term under the square root;
• the ellipticity chain Provider.DhBound.Discharge.vecNormSq_le_matrixNorm_sigmaStarInvCoarse_mul_two_mul_add keeps its cross term, so |p| ≲ λ^{-1/2} (J^{1/2} + |p·q|^{1/2}).

The resulting budget is a clean multiple of λ_{3/8,2}^{-1/2}(R) ( J(R,p,q)^{1/2} + |p·q|^{1/2} ).

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

The ellipticity chain at a general loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.vecNormSq_le_lambdaSq_inv_mul_two_mul_add {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (b : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain R)) (hG : (G.coeffOn R).AEEq b) (p q : HCPolySupport.Vec d) : HCPolySupport.vecNormSq p ≤ (HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹ * (2 * (HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) b p q + |HCPolySupport.vecDot p q|))

The ellipticity chain at a general triadic cube and a general loading.

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.vecNorm_le_sqrt_two_mul_sqrt_add {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) (G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (b : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain R)) (hG : (G.coeffOn R).AEEq b) (p q : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm p ≤ √2 * (√(HCPolySupport.Book.Ch02.lambdaSq R (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) G)⁻¹ * (√(HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) b p q) + √|HCPolySupport.vecDot p q|))

The loading budget at a general triadic cube and a general loading.

The adjoint budget at a general loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.sqrt_add_two_mul_vecDot_le {J t : ℝ} (hJ : 0 ≤ J) : √(J + 2 * t) ≤ √J + √2 * √|t|

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.cubeBesovNegativeVectorSeminormTwo_cubeAdjointGrad_pq_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {p q : 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 p (-q) 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) p q) + √2 * √|HCPolySupport.vecDot p q|))

The adjoint budget at a general loading.

The witness budget at a general loading

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.pqWitnessConst : ℝ

The explicit constant of the general-loading witness-gradient negative Besov budget.

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.pqWitnessConst_nonneg : 0 ≤ pqWitnessConst

theorem Algsuperdiff.Section24.Sensitivity.Provider.ResponseUnconditional.cubeBesovNegativeVectorSeminormTwo_pqWitnessGrad_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (p q : 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 p (-q) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p q 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) + p) : (HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q (3 / 8) fun (x : HCPolySupport.Vec d) => u.grad x) ≤ pqWitnessConst * (√(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) p q) + √|HCPolySupport.vecDot p q|))

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