English
A modular-type inequality for collapse holds, provided a ∉ u and certain linear-order and disjointness hypotheses; it bounds products of collapses by collapses of composite structures 𝒜 ⊼ ℬ and 𝒜 ⊻ ℬ.
Русский
Условно-модульное неравенство для collapse: произведение collapses оценивается через collapses симплексных структур 𝒜 ⊼ ℬ и 𝒜 ⊻ ℬ.
LaTeX
$$collapse_modular(…) inequality$$
Lean4
theorem collapse_modular [ExistsAddOfLE β] (hu : a ∉ u) (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
(h : ∀ ⦃s⦄, s ⊆ insert a u → ∀ ⦃t⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t))
(𝒜 ℬ : Finset (Finset α)) :
∀ ⦃s⦄,
s ⊆ u →
∀ ⦃t⦄,
t ⊆ u →
collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t) :=
by
rintro s hsu t htu
have := hsu.trans <| subset_insert a _
have := htu.trans <| subset_insert a _
have := insert_subset_insert a hsu
have := insert_subset_insert a htu
have has := notMem_mono hsu hu
have hat := notMem_mono htu hu
have : a ∉ s ∩ t := notMem_mono (inter_subset_left.trans hsu) hu
have := notMem_union.2 ⟨has, hat⟩
rw [collapse_eq has]
split_ifs
· rw [collapse_eq hat]
split_ifs
· rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›) rfl (insert_inter_distrib _ _ _).symm,
collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl (insert_union_distrib _ _ _).symm]
refine ineq (h₁ _) (h₁ _) (h₂ _) (h₂ _) (h₃ _) (h₃ _) (h₄ _) (h₄ _) (h ‹_› ‹_›) ?_ ?_ ?_
· simpa [*] using h ‹insert a s ⊆ _› ‹t ⊆ _›
· simpa [*] using h ‹s ⊆ _› ‹insert a t ⊆ _›
· simpa [*] using h ‹insert a s ⊆ _› ‹insert a t ⊆ _›
· rw [add_zero, add_mul]
refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_
rw [collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl (insert_union _ _ _),
insert_inter_of_notMem ‹_›, ← mul_add]
gcongr
exacts [add_nonneg (h₄ _) <| h₄ _, le_collapse_of_mem ‹_› h₃ rfl <| inter_mem_infs ‹_› ‹_›]
· rw [zero_add, add_mul]
refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_
rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›) (inter_insert_of_notMem ‹_›)
(insert_inter_distrib _ _ _).symm,
union_insert, insert_union_distrib, ← add_mul]
gcongr
exacts [add_nonneg (h₃ _) <| h₃ _,
le_collapse_of_insert_mem ‹_› h₄ (insert_union_distrib _ _ _).symm (union_mem_sups ‹_› ‹_›)]
· rw [add_zero, mul_zero]
exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _
· rw [add_zero, collapse_eq hat, mul_add]
split_ifs
· refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_
rw [collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl (union_insert _ _ _),
inter_insert_of_notMem ‹_›, ← mul_add]
exact
mul_le_mul_of_nonneg_right (le_collapse_of_mem ‹_› h₃ rfl <| inter_mem_infs ‹_› ‹_›) <|
add_nonneg (h₄ _) <| h₄ _
· rw [mul_zero, add_zero]
exact
(h ‹_› ‹_›).trans <|
mul_le_mul (le_collapse_of_mem ‹_› h₃ rfl <| inter_mem_infs ‹_› ‹_›)
(le_collapse_of_mem ‹_› h₄ rfl <| union_mem_sups ‹_› ‹_›) (h₄ _) <|
collapse_nonneg h₃ _
· rw [mul_zero, zero_add]
refine
(h ‹_› ‹_›).trans <|
mul_le_mul ?_ (le_collapse_of_insert_mem ‹_› h₄ (union_insert _ _ _) <| union_mem_sups ‹_› ‹_›) (h₄ _) <|
collapse_nonneg h₃ _
exact
le_collapse_of_mem (notMem_mono inter_subset_left ‹_›) h₃ (inter_insert_of_notMem ‹_›) <| inter_mem_infs ‹_› ‹_›
· simp_rw [mul_zero, add_zero]
exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _
· rw [zero_add, collapse_eq hat, mul_add]
split_ifs
· refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_
rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›) (insert_inter_of_notMem ‹_›)
(insert_inter_distrib _ _ _).symm,
insert_inter_of_notMem ‹_›, ← insert_inter_distrib, insert_union, insert_union_distrib, ← add_mul]
exact
mul_le_mul_of_nonneg_left
(le_collapse_of_insert_mem ‹_› h₄ (insert_union_distrib _ _ _).symm <| union_mem_sups ‹_› ‹_›) <|
add_nonneg (h₃ _) <| h₃ _
· rw [mul_zero, add_zero]
refine
(h ‹_› ‹_›).trans <|
mul_le_mul (le_collapse_of_mem ‹_› h₃ (insert_inter_of_notMem ‹_›) <| inter_mem_infs ‹_› ‹_›)
(le_collapse_of_insert_mem ‹_› h₄ (insert_union _ _ _) <| union_mem_sups ‹_› ‹_›) (h₄ _) <|
collapse_nonneg h₃ _
· rw [mul_zero, zero_add]
exact
(h ‹_› ‹_›).trans <|
mul_le_mul (le_collapse_of_insert_mem ‹_› h₃ (insert_inter_distrib _ _ _).symm <| inter_mem_infs ‹_› ‹_›)
(le_collapse_of_insert_mem ‹_› h₄ (insert_union_distrib _ _ _).symm <| union_mem_sups ‹_› ‹_›) (h₄ _) <|
collapse_nonneg h₃ _
· simp_rw [mul_zero, add_zero]
exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _
· simp_rw [add_zero, zero_mul]
exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _
