OAI/NumberTheory/Ostmann/Construction/InjectiveCoefficientTransport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transport of coefficients along an injective character reduction

  1. def OAI.Ostmann.injectiveCoefficient line 10
  2. theorem OAI.Ostmann.injectiveCoefficient_apply line 13
  3. theorem OAI.Ostmann.injectiveCoefficient_norm_le line 20
  4. theorem OAI.Ostmann.injectiveCoefficient_ne_zero line 28
  5. theorem OAI.Ostmann.injectiveCoefficient_sum line 36
  6. theorem OAI.Ostmann.sum_option_support line 48

    Source documentation

    Splitting a finite option family isolates the unique principal coefficient.

    theorem sum_option_support {β : Type*} (S : Finset (Option β)) (h : Option β → ℂ)
    (hzero : none ∉ S → h none = 0) :
    (∑ e ∈ S, h e) = h none + ∑ b ∈ S.eraseNone, h (some b) := by
…