OAI/NumberTheory/TotientAsymptotic/WeightedFiniteMap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.FiniteMap.weighted_lower line 12

   Source documentation

   A positive weight on all ordinary representatives converts a count of values into a lower bound for the weighted representation count.

   lemma weighted_lower {α β : Type*} [DecidableEq α] [DecidableEq β]
       (T D : Finset α) (W E U : Finset β) (F : α → β) (w : α → ℝ) (c : ℝ)
       (hc : 0≤c) (hU : U⊆W) (hbij : Set.BijOn F (↑(T\D)) (↑(W\E)))
       (hw : ∀ t∈T, 0≤w t)
       (hweight : ∀ t∈T\D, F t∈U → c≤w t) :
       c*((U.card : ℝ)-E.card) ≤ ∑ t∈T, w t := by
   …

   Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.w