fix most of the files

.gitignore

@@ -1,9 +1,10 @@
 
 *.olean
 /_target
-/leanpkg.path
-/build
 /doc-gen
+/build
+/leanpkg.path
+/lake-packages
 
 decls.pickle
 decls.yaml

LeanCamCombi/ErdosRenyi/Basic.lean

@@ -22,38 +22,38 @@ variable {α Ω : Type _} [MeasurableSpace Ω]
 /-- A sequence iid. real valued Bernoulli random variables with parameter `p ≤ 1`. -/
 abbrev ErdosRenyi (G : Ω → SimpleGraph α) [∀ ω, DecidableRel (G ω).Adj] (p : ℝ≥0)
     (μ : Measure Ω := by exact MeasureTheory.MeasureSpace.volume) : Prop :=
-  BernoulliSeq (fun ω ↦ (G ω).edgeSet) p μ
+  IsBernoulliSeq (fun ω ↦ (G ω).edgeSet) p μ
 
 variable (G : Ω → SimpleGraph α) (H : SimpleGraph α) [∀ ω, DecidableRel (G ω).Adj] {p : ℝ≥0}
   (μ : Measure Ω) [IsProbabilityMeasure μ] [ErdosRenyi G p μ]
 
 namespace ErdosRenyi
 
 protected lemma le_one : p ≤ 1 :=
-  BernoulliSeq.le_one (fun ω ↦ (G ω).edgeSet) μ
+  IsBernoulliSeq.le_one (fun ω ↦ (G ω).edgeSet) μ
 
 protected lemma iIndepFun : iIndepFun inferInstance (fun e ω ↦ e ∈ (G ω).edgeSet) μ :=
-  BernoulliSeq.iIndepFun _ _
+  IsBernoulliSeq.iIndepFun _ _
 
 protected lemma map (e : Sym2 α) :
     Measure.map (fun ω ↦ e ∈ (G ω).edgeSet) μ =
       (Pmf.bernoulli' p $ ErdosRenyi.le_one G μ).toMeasure :=
-  BernoulliSeq.map _ _ e
+  IsBernoulliSeq.map _ _ e
 
 protected lemma aEMeasurable (e : Sym2 α) :
     AEMeasurable (fun ω ↦ e ∈ (G ω).edgeSet) μ :=
-  BernoulliSeq.aEMeasurable _ _ e
+  IsBernoulliSeq.aEMeasurable _ _ e
 
 protected lemma nullMeasurableSet (e : Sym2 α) :
     NullMeasurableSet {ω | e ∈ (G ω).edgeSet} μ :=
-  BernoulliSeq.nullMeasurableSet _ _ e
+  IsBernoulliSeq.nullMeasurableSet _ _ e
 
 protected lemma identDistrib (d e : Sym2 α) :
     IdentDistrib (fun ω ↦ d ∈ (G ω).edgeSet) (fun ω ↦ e ∈ (G ω).edgeSet) μ μ :=
-  BernoulliSeq.identDistrib _ _ d e
+  IsBernoulliSeq.identDistrib _ _ d e
 
 lemma meas_edge (e : Sym2 α) : μ {ω | e ∈ (G ω).edgeSet} = p :=
-  BernoulliSeq.meas_apply _ _ e
+  IsBernoulliSeq.meas_apply _ _ e
 
 protected lemma meas [Fintype α] [DecidableEq α] [DecidableRel H.Adj] :
     μ {ω | G ω = H} =

LeanCamCombi/LittlewoodOfford.lean

@@ -12,11 +12,9 @@ import Mathlib.Order.Partition.Finpartition
 
 -/
 
-
 open scoped BigOperators
 
 namespace Finset
-
 variable {ι E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝒜 : Finset (Finset ι)}
   {s : Finset ι} {f : ι → E} {r : ℝ}
 
@@ -37,17 +35,16 @@ lemma exists_littlewood_offord_partition [DecidableEq ι] (hr : 0 < r) (hf : ∀
     Finset.exists_max_image _ (fun t ↦ g (∑ i in t, f i)) (P.nonempty_of_mem_parts h𝒜)
   sorry
 
-/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (u v «expr ∈ » 𝒜) -/
 /-- **Kleitman's lemma** -/
 lemma card_le_of_forall_dist_sum_le (hr : 0 < r) (h𝒜 : ∀ t ∈ 𝒜, t ⊆ s) (hf : ∀ i ∈ s, r ≤ ‖f i‖)
-    (h𝒜r : ∀ (u) (_ : u ∈ 𝒜) (v) (_ : v ∈ 𝒜), dist (∑ i in u, f i) (∑ i in v, f i) < r) :
+    (h𝒜r : ∀ u, u ∈ 𝒜 → ∀ v, v ∈ 𝒜 → dist (∑ i in u, f i) (∑ i in v, f i) < r) :
     𝒜.card ≤ s.card.choose (s.card / 2) := by
   classical
-  obtain ⟨P, hP, hs, hr⟩ := exists_littlewood_offord_partition hr hf
+  obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf
   rw [←hP]
   refine'
     card_le_card_of_forall_subsingleton (· ∈ ·) (fun t ht ↦ _) fun ℬ hℬ t ht u hu ↦
-      (hr _ hℬ).Eq ht.2 hu.2 (h𝒜r _ ht.1 _ hu.1).not_le
+      (hr _ hℬ).eq ht.2 hu.2 (h𝒜r _ ht.1 _ hu.1).not_le
   simpa only [exists_prop] using P.exists_mem (mem_powerset.2 $ h𝒜 _ ht)
 
 end Finset

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean

@@ -347,15 +347,13 @@ lemma le_card_edgeFinset_kill [Fintype β] :
   simp only [kill_of_ne_bot, hG, Ne.def, not_false_iff, Set.iUnion_singleton_eq_range,
     Set.toFinset_card, Fintype.card_ofFinset, edgeSet_deleteEdges]
   rw [←Set.toFinset_card, ←edgeFinset, copyCount, ←card_subtype, subtype_univ]
-  refine'
-    (tsub_le_tsub_left
-          (card_image_le.trans_eq' $
-            congr_arg card $
-              Set.toFinset_range fun H' : {H' : H.Subgraph // Nonempty (G ≃g H'.coe)} ↦
-                (aux hG H'.2).some)
-          _).trans
-      ((le_card_sdiff _ _).trans_eq $ congr_arg card $ coe_injective _)
-  simp only [Set.diff_eq, ←Set.iUnion_singleton_eq_range, coe_sdiff, Set.coe_toFinset, coe_filter,
-    Set.sep_mem_eq, Set.iUnion_subtype]
+  refine' (tsub_le_tsub_left (card_image_le.trans_eq' $ congr_arg card $ Set.toFinset_range
+    fun H' : {H' : H.Subgraph // Nonempty (G ≃g H'.coe)} ↦ (aux hG H'.2).some) _).trans $
+      (le_card_sdiff _ _).trans_eq $ _
+  simp only [Finset.sdiff_eq_inter_compl, Set.diff_eq, ←Set.iUnion_singleton_eq_range, coe_sdiff,
+    Set.coe_toFinset, coe_filter, Set.sep_mem_eq, Set.iUnion_subtype, ←Fintype.card_coe,
+    ←Finset.coe_sort_coe, coe_inter, coe_compl, Set.coe_toFinset]
+  congr
+  exact Subsingleton.elim _ _
 
 end SimpleGraph

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Density.lean

@@ -2,11 +2,9 @@ import Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 
 open Finset
-
 open scoped Classical
 
 namespace SimpleGraph
-
 variable {α : Type _} [Fintype α] (G : SimpleGraph α) [Fintype G.edgeSet]
 
 def fullEdgeDensity : ℚ := G.edgeFinset.card / Fintype.card α

LeanCamCombi/Mathlib/Order.lean

@@ -3,7 +3,6 @@ import Mathlib.Order.Hom.Set
 open OrderDual Set
 
 section Lattice
-
 variable {α : Type _} [Lattice α] [BoundedOrder α] {a b : α}
 
 lemma isCompl_comm : IsCompl a b ↔ IsCompl b a :=
@@ -12,11 +11,9 @@ lemma isCompl_comm : IsCompl a b ↔ IsCompl b a :=
 end Lattice
 
 section BooleanAlgebra
-
 variable {α : Type _} [BooleanAlgebra α]
 
 @[simp]
-lemma OrderIso.compl_symm_apply' (a : αᵒᵈ) : (OrderIso.compl α).symm a = ofDual aᶜ :=
-  rfl
+lemma OrderIso.compl_symm_apply' (a : αᵒᵈ) : (OrderIso.compl α).symm a = ofDual aᶜ := rfl
 
 end BooleanAlgebra

LeanCamCombi/Mathlib/Pmf.lean

@@ -2,25 +2,20 @@ import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 import Mathlib.Probability.ProbabilityMassFunction.Constructions
 
 -- TODO: On a countable space, define one-to-one correspondance between `pmf` and probability
--- TODO: On a countable space, define one-to-one correspondance between `pmf` and probability
--- measures
 -- measures
 open MeasureTheory
-
 open scoped BigOperators Classical ENNReal NNReal
 
 namespace Pmf
-
 variable {α β : Type _}
 
 section OfFintype
-
 variable [Fintype α] [Fintype β]
 
 open Finset
 
 @[simp]
-lemma map_ofFintype (f : α → ℝ≥0∞) (h : (univ.Sum fun a : α ↦ f a) = 1) (g : α → β) :
+lemma map_ofFintype (f : α → ℝ≥0∞) (h : ∑ a, f a = 1) (g : α → β) :
     (ofFintype f h).map g =
       ofFintype (fun b ↦ ∑ a in univ.filter fun a ↦ g a = b, f a)
         (by
@@ -30,13 +25,12 @@ lemma map_ofFintype (f : α → ℝ≥0∞) (h : (univ.Sum fun a : α ↦ f a) =
             refine' fun b₁ _ b₂ _ hb ↦ disjoint_left.2 fun a ha₁ ha₂ ↦ _
             simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂
             exact hb (ha₁.symm.trans ha₂)
-          rw [←sum_disj_Union _ _ this]
+          rw [←sum_disjiUnion _ _ this]
           convert h
-          exact
-            eq_univ_of_forall fun a ↦
-              mem_disj_Union.2 ⟨_, mem_univ _, mem_filter.2 ⟨mem_univ _, rfl⟩⟩) := by
+          exact eq_univ_of_forall fun a ↦
+            mem_disjiUnion.2 ⟨_, mem_univ _, mem_filter.2 ⟨mem_univ _, rfl⟩⟩) := by
   ext b : 1
-  simp only [sum_filter, eq_comm, map_apply, of_fintype_apply]
+  simp only [sum_filter, eq_comm, map_apply, ofFintype_apply]
   exact tsum_eq_sum fun _ h ↦ (h $ mem_univ _).elim
 
 end OfFintype
@@ -47,19 +41,20 @@ lemma toMeasure_ne_zero (p : Pmf α) : p.toMeasure ≠ 0 :=
   IsProbabilityMeasure.ne_zero p.toMeasure
 
 @[simp]
-lemma map_toMeasure (p : Pmf α) (hf : Measurable f) : p.toMeasure.map f = (p.map f).toMeasure := by ext s hs : 1; rw [Pmf.toMeasure_map_apply _ _ _ hf hs, measure.map_apply hf hs]
+lemma map_toMeasure (p : Pmf α) (hf : Measurable f) : p.toMeasure.map f = (p.map f).toMeasure := by
+  ext s hs : 1; rw [Pmf.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]
 
 section bernoulli
 
 /-- A `pmf` which assigns probability `p` to true propositions and `1 - p` to false ones. -/
 noncomputable def bernoulli' (p : ℝ≥0) (h : p ≤ 1) : Pmf Prop :=
-  (ofFintype fun b ↦ if b then p else 1 - p) $ by norm_cast; exact NNReal.eq (by simp [h])
+  (ofFintype fun b ↦ if b then p else 1 - p) $ by simp_rw [←ENNReal.coe_one, ←ENNReal.coe_sub,
+    ←apply_ite ((↑) : ℝ≥0 → ℝ≥0∞), ←ENNReal.coe_finset_sum, ENNReal.coe_eq_coe]; simp [h]
 
 variable {p : ℝ≥0} (hp : p ≤ 1) (b : Prop)
 
 @[simp]
-lemma bernoulli'_apply : bernoulli' p hp b = if b then p else 1 - p :=
-  rfl
+lemma bernoulli'_apply : bernoulli' p hp b = if b then (p : ℝ≥0∞) else 1 - p := rfl
 
 @[simp]
 lemma support_bernoulli' : (bernoulli' p hp).support = {b | if b then p ≠ 0 else p ≠ 1} :=
@@ -69,16 +64,16 @@ lemma mem_support_bernoulli'_iff : b ∈ (bernoulli' p hp).support ↔ if b then
 
 @[simp]
 lemma map_not_bernoulli' : (bernoulli' p hp).map Not = bernoulli' (1 - p) tsub_le_self := by
-  have : ∀ p : Prop, (finset.univ.filter fun q : Prop ↦ ¬ q ↔ p) = {¬ p} := by
+  have : ∀ p : Prop, (Finset.univ.filter fun q : Prop ↦ ¬ q ↔ p) = {¬ p} := by
     rintro p
-    ext q by_cases p <;> by_cases q <;> simp [*]
-  refine' (map_of_fintype _ _ _).trans _
-  simp only [this, -Fintype.univ_Prop, bernoulli', Finset.mem_filter, Finset.mem_univ, true_and_iff,
+    ext q
+    by_cases p <;> by_cases q <;> simp [*]
+  refine' (map_ofFintype _ _ _).trans _
+  simp only [this, bernoulli', Finset.mem_filter, Finset.mem_univ, true_and_iff,
     Finset.mem_disjiUnion, tsub_le_self, eq_iff_iff, Finset.sum_singleton, WithTop.coe_sub,
     ENNReal.coe_one]
-  congr 1 with p
-  rw [ENNReal.sub_sub_cancel WithTop.one_ne_top (ENNReal.coe_le_coe.2 hp)]
-  split_ifs <;> rfl
+  congr 1 with q
+  split_ifs <;> simp [ENNReal.sub_sub_cancel WithTop.one_ne_top (ENNReal.coe_le_coe.2 hp)]
 
 end bernoulli
 

LeanCamCombi/Mathlib/Probability/Independence.lean → LeanCamCombi/Mathlib/Probability/Independence/Basic.lean

@@ -2,7 +2,6 @@ import Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 
 open MeasureTheory MeasurableSpace Set
-
 open scoped BigOperators
 
 namespace ProbabilityTheory
@@ -34,8 +33,8 @@ lemma iIndepSet_iff_iIndepSets_singleton {s : ι → Set Ω} (hs : ∀ i, Measur
     (μ : Measure Ω := by volume_tac) [IsProbabilityMeasure μ] :
     iIndepSet s μ ↔ iIndepSets (fun i ↦ {s i}) μ :=
   ⟨iIndep.iIndepSets fun _ ↦ rfl,
-    IndepSets.indep _ _ _
-      (IsPiSystem.singleton $ s _) _ _⟩
+    iIndepSets.iIndep _ (fun i => generateFrom_le <| by rintro t (rfl : t = s i); exact hs _) _
+      (fun _ => IsPiSystem.singleton <| s _) fun _ => rfl⟩
 
 variable [IsProbabilityMeasure μ]
 

LeanCamCombi/VanDenBergKesten.lean

@@ -34,16 +34,14 @@ open scoped Classical FinsetFamily
 variable {α : Type _}
 
 namespace Finset
-
 section BooleanAlgebra
-
 variable [BooleanAlgebra α] (s t u : Finset α) {a : α}
 
 noncomputable def certificator : Finset α :=
   (s ∩ t).filter fun a ↦
     ∃ x y, IsCompl x y ∧ (∀ ⦃b⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b⦄, a ⊓ y = b ⊓ y → b ∈ t
 
-scoped[FinsetFamily] infixl:70 " □ " ↦ certificator
+scoped[FinsetFamily] infixl:70 " □ " => Finset.certificator
 
 variable {s t u}
 
@@ -52,14 +50,14 @@ lemma mem_certificator :
     a ∈ s □ t ↔
       ∃ x y, IsCompl x y ∧ (∀ ⦃b⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b⦄, a ⊓ y = b ⊓ y → b ∈ t := by
   rw [certificator, mem_filter, and_iff_right_of_imp]
-  rintro ⟨u, v, huv, hu, hv⟩
+  rintro ⟨u, v, _, hu, hv⟩
   exact mem_inter.2 ⟨hu rfl, hv rfl⟩
 
 lemma certificator_subset_inter : s □ t ⊆ s ∩ t :=
   filter_subset _ _
 
 lemma certificator_subset_disjSups : s □ t ⊆ s ○ t := by
-  simp_rw [subset_iff, mem_certificator, mem_disj_sups]
+  simp_rw [subset_iff, mem_certificator, mem_disjSups]
   rintro x ⟨u, v, huv, hu, hv⟩
   refine'
     ⟨x ⊓ u, hu inf_right_idem.symm, x ⊓ v, hv inf_right_idem.symm,
@@ -68,30 +66,30 @@ lemma certificator_subset_disjSups : s □ t ⊆ s ○ t := by
 
 variable (s t u)
 
-lemma certificator_comm : s □ t = t □ s := by ext s; rw [mem_certificator, exists_comm];
-  simp [isCompl_comm, and_comm']
+lemma certificator_comm : s □ t = t □ s := by
+  ext s; rw [mem_certificator, exists_comm]; simp [isCompl_comm, and_comm]
 
 lemma IsUpperSet.certificator_eq_inter (hs : IsUpperSet (s : Set α))
     (ht : IsLowerSet (t : Set α)) : s □ t = s ∩ t := by
   refine'
     certificator_subset_inter.antisymm fun a ha ↦ mem_certificator.2 ⟨a, aᶜ, isCompl_compl, _⟩
   rw [mem_inter] at ha
-  simp only [@eq_comm _ ⊥, ←sdiff_eq, inf_idem, right_eq_inf, sdiff_self, sdiff_eq_bot_iff]
+  simp only [@eq_comm _ ⊥, ←sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff]
   exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
 
 lemma IsLowerSet.certificator_eq_inter (hs : IsLowerSet (s : Set α))
     (ht : IsUpperSet (t : Set α)) : s □ t = s ∩ t := by
   refine'
     certificator_subset_inter.antisymm fun a ha ↦
-      mem_certificator.2 ⟨aᶜ, a, is_compl_compl.symm, _⟩
+      mem_certificator.2 ⟨aᶜ, a, isCompl_compl.symm, _⟩
   rw [mem_inter] at ha
-  simp only [@eq_comm _ ⊥, ←sdiff_eq, inf_idem, right_eq_inf, sdiff_self, sdiff_eq_bot_iff]
+  simp only [@eq_comm _ ⊥, ←sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff]
   exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩
 
 lemma IsUpperSet.certificator_eq_disjSups (hs : IsUpperSet (s : Set α))
     (ht : IsUpperSet (t : Set α)) : s □ t = s ○ t := by
-  refine' certificator_subset_disj_sups.antisymm fun a ha ↦ mem_certificator.2 _
-  obtain ⟨x, hx, y, hy, hxy, rfl⟩ := mem_disj_sups.1 ha
+  refine' certificator_subset_disjSups.antisymm fun a ha ↦ mem_certificator.2 _
+  obtain ⟨x, hx, y, hy, hxy, rfl⟩ := mem_disjSups.1 ha
   refine' ⟨x, xᶜ, isCompl_compl, _⟩
   simp only [inf_of_le_right, le_sup_left, right_eq_inf, ←sdiff_eq, hxy.sup_sdiff_cancel_left]
   exact ⟨fun b hab ↦ hs hab hx, fun b hab ↦ ht (hab.trans_le sdiff_le) hy⟩