card_biUnion_star_le_m_add_one_card_star_mul

English

A bound comparing the sum over star-parts products to the sum over chunk-parts products, controlled by 16^{|P.parts|}.

Русский

Сравнение суммы по произведениям звезд-сегментов с суммой по частям chunk, управляемое 16^{|P.parts|}.

LaTeX

$$Sum over star hP G ε hU V of density^2 ≤ Sum over chunk hP G ε hU · chunk hP G ε hV of density^2 divided by 16^{|P.parts|}.$$

Lean4

theorem card_biUnion_star_le_m_add_one_card_star_mul :
    (#((star hP G ε hU V).biUnion id) : ℝ) ≤ #(star hP G ε hU V) * (m + 1) :=
  mod_cast card_biUnion_le_card_mul _ _ _ fun _ hs => card_le_m_add_one_of_mem_chunk_parts <| star_subset_chunk hs

Похожие утверждения