Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.Table4Ext.xhalfCurve_sub_supported

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row4 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean:118 to 131

Source documentation

Support of lhsE - xhalfCurveE c twoK for the dyadic slab kernel.

Exact Lean statement

lemma xhalfCurve_sub_supported (c : ℚ) (twoK : ℕ) :
    ExprSupportedWithInv (Expr.sub FloorButhe.lhsE (xhalfCurveE c twoK))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma xhalfCurve_sub_supported (c : ℚ) (twoK : ℕ) :    ExprSupportedWithInv (Expr.sub FloorButhe.lhsE (xhalfCurveE c twoK)) := by  refine ExprSupportedWithInv.add ?_ (ExprSupportedWithInv.neg ?_)  · show ExprSupportedWithInv FloorButhe.lhsE    simp only [FloorButhe.lhsE, FloorButhe.pow8, FloorButhe.sqx, FloorButhe.s2,      FloorButhe.s4, FloorButhe.e2]    repeat constructor  · unfold xhalfCurveE    refine ExprSupportedWithInv.mul (ExprSupportedWithInv.const _) ?_    refine ExprSupportedWithInv.mul (pow_supported (ExprSupportedWithInv.var 0) twoK) ?_    unfold expSplitNegXpow    iterate 6 apply sqE_supported    exact ExprSupportedWithInv.exp (ExprSupportedWithInv.mul (ExprSupportedWithInv.const _)      (ExprSupportedWithInv.mul (ExprSupportedWithInv.var _) (ExprSupportedWithInv.var _)))