DoubledPairingSolutions

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

The Poincare carriers are the gauged doubled field and its gauged flux

Source displays in ABK26:

• e.findSfull and e.bfS, the characterization of the double-variable solution space S(cu_m) used in Remark r.cg.poincare.doubled.variables;

• e.bfA.magic.swapping,

  bfA ( p + p^* , a p - a^t p^* ) = ( a p + a^t p^* , p - p^* );
  

• e.CG.Poincare.doubled.vars, whose two left-hand seminorms are taken of bfA_0^{1/2} X and bfA_0^{-1/2} bfA X.

What the module supplies

DoubledCoarsePoincare.lean proves the doubled Poincare inequality with its two left-hand sides written as the explicit fields doubledStateField and doubledFluxField of a primal/adjoint cube-solution pair. The Step-2 consumer, by contrast, holds a doubled field X and needs the seminorms of bfA_0^{1/2}X and bfA_0^{-1/2} bfA_m X in the gauge vocabulary of DoubledPairingGauge.lean.

The two are literally the same objects:

• the state carrier needs no lemma at all: doubledStateField is, by definition, blockGaugeUp -- that is bfA_0^{1/2} -- applied to Ch02.doubledFieldOfSolutions;
• doubledFluxField_apply_eq_blockGaugeDown -- doubledFluxField is bfA_0^{-1/2} applied to bfA applied to the same field, by e.bfA.magic.swapping.

Together they identify the manuscript's [bfAhom^{-1/2} bfA_m tilde S_z]_{H^{-1}} with the quantity the proved Poincare inequality actually bounds, which is the hpoin leg of PerCubeFluctuationArithmetic.perCube_fluct_le.

sqrt_mul_add_inv_sqrt_mul_sq_le_two_mul records the remaining arithmetic link: the Poincare ellipticity factor squares to at most twice the gaugedEllipticitySum of LocalizationFluctuationEllipticity.lean, which is the form in which carry it.

Binders

0 < sig0 is the positivity of the scalar sigma_0 of e.form.of.A.naught; hdet (or the ambient ellipticity that supplies it) is the invertibility of the symmetric part at the point, which is what makes bfA the matrix of e.block.matrix.basic.definitions there. No smallness, moment or measurability proposition occurs.

Scope

No anchor, frozen theorem or external input is consumed, and there is no sorry.

The state carrier is the gauged doubled field

doubledStateField sig0 Q a v vStar x unfolds to blockGaugeUp sig0 of (Ch02.doubledFieldOfSolutions (a.coeffOn Q) v vStar).eval x, so the first of the two identifications holds by definition and carries no statement here.

The flux carrier is the gauged image under bfA

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockMatVecMul_blockMatrixField_doubledFieldOfSolutions {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (v : HCPolySupport.Book.Ch03.CubeSolution Q a) (vStar : HCPolySupport.Book.Ch03.CubeSolution Q (adjointFamily a)) {x : HCPolySupport.Vec d} (hdet : IsUnit (Matrix.det (HCPolySupport.symmPart ((a.coeffOn Q).toCoeffField x)))) : HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField (a.coeffOn Q) x) ((HCPolySupport.Book.Ch02.doubledFieldOfSolutions (a.coeffOn Q) v vStar).eval x) = (HCPolySupport.Book.Ch03.solutionFluxField Q a v x + HCPolySupport.Book.Ch03.solutionFluxField Q (adjointFamily a) vStar x, HCPolySupport.Book.Ch03.solutionGradientField v x - HCPolySupport.Book.Ch03.solutionGradientField vStar x)

e.bfA.magic.swapping at a point. Applying the doubled matrix of a to the doubled field of a solution pair swaps the two legs.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.doubledFluxField_apply_eq_blockGaugeDown {d : ℕ} (sig0 : ℝ) (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (v : HCPolySupport.Book.Ch03.CubeSolution Q a) (vStar : HCPolySupport.Book.Ch03.CubeSolution Q (adjointFamily a)) {x : HCPolySupport.Vec d} (hdet : IsUnit (Matrix.det (HCPolySupport.symmPart ((a.coeffOn Q).toCoeffField x)))) : doubledFluxField sig0 Q a v vStar x = blockGaugeDown sig0 (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixField (a.coeffOn Q) x) ((HCPolySupport.Book.Ch02.doubledFieldOfSolutions (a.coeffOn Q) v vStar).eval x))

bfA_0^{-1/2} bfA X for X the doubled field of a solution pair. The second left-hand carrier of e.CG.Poincare.doubled.vars is the down-gauge of the bfA-image of e.findSfull's field.

This is the identification the Step-2 consumer needs: the manuscript's [bfAhom^{-1/2} bfA_m tilde S_z]_{H^{-1}} is a seminorm of exactly the field that DoubledCoarsePoincare.doubledCoarsePoincare_le_doubledEnergy bounds.

The Poincare ellipticity factor against the gauged ellipticity sum

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.sqrt_mul_add_inv_sqrt_mul_sq_le_two_mul {sig0 lamInv Lam : ℝ} (hsig0 : 0 < sig0) (hlamInv : 0 ≤ lamInv) (hLam : 0 ≤ Lam) : (√sig0 * √lamInv + (√sig0)⁻¹ * √Lam) * (√sig0 * √lamInv + (√sig0)⁻¹ * √Lam) ≤ 2 * (sig0⁻¹ * Lam + sig0 * lamInv)

The arithmetic link. The ellipticity factor carried by e.CG.Poincare.doubled.vars,

Theta_0 = sigma_0^{1/2} lambda_{s,2}^{-1/2} + sigma_0^{-1/2} Lambda_{s,2}^{1/2} ,

satisfies Theta_0^2 <= 2 (sigma_0^{-1} Lambda_{s,2} + sigma_0 lambda_{s,2}^{-1}), i.e. Theta_0 <= sqrt 2 * sqrt (gaugedEllipticitySum sigma_0.). This is what turns the square root of the ellipticity sum appearing in the Poincare factor into the first power appearing: the factor is spent twice in the quadratic term and twice in the cross term.