English
Let A, B, C be finite subsets of a group G. If for every A' ⊆ A we have |A B| · |A'| ≤ |A' B| · |A|, then |C A B| · |A| ≤ |A B| · |C A|.
Русский
Пусть A, B, C — конечные подмножества группы G. Если для каждого A' ⊆ A выполняется |A B| · |A'| ≤ |A' B| · |A|, то |C A B| · |A| ≤ |A B| · |C A|.
LaTeX
$$$|C A B|\,|A| \le |A B|\,|C A|$$$
Lean4
@[to_additive]
theorem pluennecke_petridis_inequality_mul (C : Finset G) (hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A) :
#(C * A * B) * #A ≤ #(A * B) * #(C * A) := by
induction C using Finset.induction_on with
| empty => simp
| insert x C _ ih =>
set A' := A ∩ ({ x }⁻¹ * C * A) with hA'
set C' := insert x C with hC'
have h₀ : { x } * A' = { x } * A ∩ (C * A) := by
rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
have h₁ : C' * A * B = C * A * B ∪ ({ x } * A * B) \ ({ x } * A' * B) :=
by
rw [hC', insert_eq, union_comm, union_mul, union_mul]
refine (sup_sdiff_eq_sup ?_).symm
rw [h₀]
gcongr
exact inter_subset_right
have h₂ : { x } * A' * B ⊆ { x } * A * B := by gcongr; exact inter_subset_left
have h₃ : #(C' * A * B) ≤ #(C * A * B) + #(A * B) - #(A' * B) :=
by
rw [h₁]
refine (card_union_le _ _).trans_eq ?_
rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_}, mul_assoc {_},
card_singleton_mul, card_singleton_mul]
refine (mul_le_mul_right' h₃ _).trans ?_
rw [tsub_mul, add_mul]
refine (tsub_le_tsub (add_le_add_right ih _) <| hA _ inter_subset_left).trans_eq ?_
rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A, ← card_singleton_mul x A',
add_comm #_, h₀, eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
