Growth in the quotient and intersection with a subgroup

For a group G and a subgroup H ≤ G, this file upper and lower bounds the growth of a finset by its growth in H and G ⧸ H.

theorem Finset.card_pow_quotient_mul_pow_inter_subgroup_le {G : Type u_1} [Group G] [DecidableEq G] {H : Subgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} {m n : ℕ} : (Finset.image (⇑(QuotientGroup.mk' H)) (A ^ m)).card * (Finset.filter (fun (x : G) => x ∈ H) (A ^ n)).card ≤ (A ^ (m + n)).card

theorem Finset.card_nsmul_quotient_add_nsmul_inter_addSubgroup_le {G : Type u_1} [AddGroup G] [DecidableEq G] {H : AddSubgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} {m n : ℕ} : (Finset.image (⇑(QuotientAddGroup.mk' H)) (m • A)).card * (Finset.filter (fun (x : G) => x ∈ H) (n • A)).card ≤ ((m + n) • A).card

theorem Finset.le_card_quotient_mul_sq_inter_subgroup {G : Type u_1} [Group G] [DecidableEq G] {H : Subgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} (hAsymm : A⁻¹ = A) : A.card ≤ (Finset.image (⇑(QuotientGroup.mk' H)) A).card * (Finset.filter (fun (x : G) => x ∈ H) (A ^ 2)).card

theorem Finset.le_card_quotient_add_sq_inter_addSubgroup {G : Type u_1} [AddGroup G] [DecidableEq G] {H : AddSubgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} (hAsymm : -A = A) : A.card ≤ (Finset.image (⇑(QuotientAddGroup.mk' H)) A).card * (Finset.filter (fun (x : G) => x ∈ H) (2 • A)).card