Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.Table4Ext.lhsE_sub_negxpow_supported

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row11 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean:228 to 238

Source documentation

Support of lhsE - expSplitNegXpow n for the dyadic slab kernel.

Exact Lean statement

lemma lhsE_sub_negxpow_supported (n : ℕ) :
    ExprSupportedWithInv (Expr.sub FloorButhe.lhsE (expSplitNegXpow n))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lhsE_sub_negxpow_supported (n : ℕ) :    ExprSupportedWithInv (Expr.sub FloorButhe.lhsE (expSplitNegXpow n)) := 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 expSplitNegXpow    iterate 6 apply sqE_supported    exact ExprSupportedWithInv.exp (ExprSupportedWithInv.mul (ExprSupportedWithInv.const _)      (ExprSupportedWithInv.mul (ExprSupportedWithInv.var _) (ExprSupportedWithInv.var _)))