CubeWitness

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

The zero-trace witness budget at the pure-potential loading

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

At q = 0 the source combination is

∇u = ½ (∇v(·,R,p,0;a) + ∇v(·,R,p,0;aᵗ)) + p ,

so there are three summands. The two maximizer gradients are handled by the general-cube budget of Provider.Lambda.WitnessBudget; because the pure-potential response is transpose invariant (BigLambda.responseJ_potential_transpose) the adjoint half carries no |p·q| shift. The affine summand p is a constant field, whose negative Besov seminorm is ≤ C |p| (Discharge.ConstantBesov), and |p| is absorbed by the general-cube ellipticity chain (BigLambda.vecNorm_le_sqrt_two_mul_sqrt_lambdaSq_inv_mul_sqrt_responseJ).

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

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

The adjoint budget at the pure-potential loading

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.cubeBesovNegativeVectorSeminormTwo_cubeAdjointGrad_potential_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {p : 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 (-0) 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 0))

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

The pure-potential witness budget

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potWitnessConst : ℝ

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

Equations

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.potWitnessConst_nonneg : 0 ≤ potWitnessConst

theorem Algsuperdiff.Section24.Sensitivity.Provider.BigLambda.cubeBesovNegativeVectorSeminormTwo_potWitnessGrad_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (p : 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 (-0) vAdj) (hv : HCPolySupport.Book.Ch02.IsResponseMaximizer (HCPolySupport.Book.Ch02.cubeDomain Q) (F.coeffOn Q) p 0 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) ≤ potWitnessConst * (√(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 0))

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