𝕜 : Type ?u.36968
ι : Type ?u.36971
κ : Type ?u.36974
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity r s₁ t₁ - edgeDensity r s₂ t₂ ≤ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
𝕜 : Type ?u.36968
ι : Type ?u.36971
κ : Type ?u.36974
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ abs (edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁) ≤ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
refine' abs_sub_le_iff.2 ⟨edgeDensity_sub_edgeDensity_le_one_sub_mul r hs ht hs₂ ht₂, _⟩
𝕜 : Type ?u.36968
ι : Type ?u.36971
κ : Type ?u.36974
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity (fun x y => ¬r x y) s₂ t₂ - edgeDensity (fun x y => ¬r x y) s₁ t₁ ≤
    1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
𝕜 : Type ?u.36968
ι : Type ?u.36971
κ : Type ?u.36974
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity r s₁ t₁ - edgeDensity r s₂ t₂ ≤ 1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
rw [← add_sub_cancel (edgeDensity r s₁ t₁) (edgeDensity (fun x y ↦ ¬r x y) s₁ t₁),
  ← add_sub_cancel (edgeDensity r s₂ t₂) (edgeDensity (fun x y ↦ ¬r x y) s₂ t₂),
  edgeDensity_add_edgeDensity_compl _ (hs₂.mono hs) (ht₂.mono ht),
  edgeDensity_add_edgeDensity_compl _ hs₂ ht₂, sub_sub_sub_cancel_left]
no goals
𝕜 : Type ?u.36968
ι : Type ?u.36971
κ : Type ?u.36974
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s₁ s₂ : Finset α
t t₁ t₂ : Finset β
a : α
b : β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : Finset.Nonempty s₂
ht₂ : Finset.Nonempty t₂
⊢ edgeDensity (fun x y => ¬r x y) s₂ t₂ - edgeDensity (fun x y => ¬r x y) s₁ t₁ ≤
    1 - ↑(card s₂) / ↑(card s₁) * (↑(card t₂) / ↑(card t₁))
exact edgeDensity_sub_edgeDensity_le_one_sub_mul _ hs ht hs₂ ht₂