∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {t : E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [MeasureTheory.IsProbabilityMeasure μ], ‖1 - MeasureTheory.charFun μ t‖ ≤ 2