feat(combinatorics/simple_graph/density): positivity extension for …

…`edge_density` (#16640)

Add a `positivity` extension for `rel.edge_density` and `simple_graph.edge_density`.

Also golf the file a little using `positivity`.

src/combinatorics/simple_graph/density.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import combinatorics.simple_graph.basic
 import order.partition.finpartition
+import tactic.positivity
 
 /-!
 # Edge density
@@ -163,7 +164,7 @@ begin
   refine (sub_le_sub_left (mul_edge_density_le_edge_density r hs ht hs₂ ht₂) _).trans _,
   refine le_trans _ (mul_le_of_le_one_right _ (edge_density_le_one r s₂ t₂)),
   { rw [sub_mul, one_mul] },
-  refine sub_nonneg_of_le (mul_le_one _ (div_nonneg (nat.cast_nonneg _) (nat.cast_nonneg _)) _);
+  refine sub_nonneg_of_le (mul_le_one _ (by positivity) _);
   exact div_le_one_of_le (nat.cast_le.2 (card_le_of_subset ‹_›)) (nat.cast_nonneg _),
 end
 
@@ -203,7 +204,7 @@ begin
   apply sub_le_sub_left (mul_le_mul ((le_div_iff _).2 hs₂) ((le_div_iff _).2 ht₂) hδ₁.le _),
   { exact_mod_cast (hs₂'.mono hs).card_pos },
   { exact_mod_cast (ht₂'.mono ht).card_pos },
-  { exact div_nonneg (nat.cast_nonneg _) (nat.cast_nonneg _) }
+  { positivity }
 end
 
 /-- If `s₂ ⊆ s₁`, `t₂ ⊆ t₁` and they take up all but a `δ`-proportion, then the difference in edge
@@ -349,3 +350,19 @@ lemma edge_density_comm (s t : finset α) : G.edge_density s t = G.edge_density
 edge_density_comm G.symm s t
 
 end simple_graph
+
+namespace tactic
+open positivity
+
+/-- Extension for the `positivity` tactic: `rel.edge_density` and `simple_graph.edge_density` are
+always nonnegative. -/
+@[positivity]
+meta def positivity_edge_density : expr → tactic strictness
+| `(rel.edge_density %%r %%s %%t) := nonnegative <$>
+                                       mk_mapp ``rel.edge_density_nonneg [none, none, r, none, s, t]
+| `(simple_graph.edge_density %%G %%s %%t) := nonnegative <$>
+                                    mk_mapp ``simple_graph.edge_density_nonneg [none, G, none, s, t]
+| e := pp e >>= fail ∘ format.bracket "The expression `"
+    "` isn't of the form `rel.edge_density r s t` nor `simple_graph.edge_density G s t`"
+
+end tactic

test/positivity.lean

@@ -1,6 +1,7 @@
 import algebra.order.smul
 import analysis.normed.group.basic
 import analysis.special_functions.pow
+import combinatorics.simple_graph.density
 import data.complex.exponential
 import data.rat.nnrat
 import data.real.ereal
@@ -134,6 +135,11 @@ example {X : Type*} [metric_space X] (x y : X) : 0 ≤ dist x y := by positivity
 example {E : Type*} [add_group E] {p : add_group_seminorm E} {x : E} : 0 ≤ p x := by positivity
 example {E : Type*} [group E] {p : group_seminorm E} {x : E} : 0 ≤ p x := by positivity
 
+example {r : α → β → Prop} [Π a, decidable_pred (r a)] {s : finset α} {t : finset β} :
+  0 ≤ rel.edge_density r s t := by positivity
+example {G : simple_graph α} [decidable_rel G.adj] {s t : finset α} :
+  0 ≤ G.edge_density s t := by positivity
+
 /- ### Canonical orders -/
 
 example {a : ℕ} : 0 ≤ a := by positivity