Theorems · Definition · number theory

WeakFEPair.f_modif

{E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℝ → E

Piecewise modified version of f with optimal asymptotics. We deliberately choose intervals which don't quite join up, so the function is 0 at x = 1, in order to maintain symmetry; there is no "good" choice of value at 1.

Defined in

Mathlib.NumberTheory.LSeries.AbstractFuncEq

Cited by

6 results in Mathlib

Foundations

Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace