bump to nightly-2023-06-08-07

mathlib commit leanprover-community/mathlib@31c24aa

Mathbin/Analysis/NormedSpace/Enorm.lean

@@ -42,39 +42,43 @@ attribute [local instance 1001] Classical.propDecidable
 
 open scoped ENNReal
 
+#print ENorm /-
 /-- Extended norm on a vector space. As in the case of normed spaces, we require only
 `‖c • x‖ ≤ ‖c‖ * ‖x‖` in the definition, then prove an equality in `map_smul`. -/
-structure Enorm (𝕜 : Type _) (V : Type _) [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] where
+structure ENorm (𝕜 : Type _) (V : Type _) [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] where
   toFun : V → ℝ≥0∞
   eq_zero' : ∀ x, to_fun x = 0 → x = 0
   map_add_le' : ∀ x y : V, to_fun (x + y) ≤ to_fun x + to_fun y
   map_smul_le' : ∀ (c : 𝕜) (x : V), to_fun (c • x) ≤ ‖c‖₊ * to_fun x
-#align enorm Enorm
+#align enorm ENorm
+-/
 
-namespace Enorm
+namespace ENorm
 
-variable {𝕜 : Type _} {V : Type _} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : Enorm 𝕜 V)
+variable {𝕜 : Type _} {V : Type _} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENorm 𝕜 V)
 
-instance : CoeFun (Enorm 𝕜 V) fun _ => V → ℝ≥0∞ :=
-  ⟨Enorm.toFun⟩
+instance : CoeFun (ENorm 𝕜 V) fun _ => V → ℝ≥0∞ :=
+  ⟨ENorm.toFun⟩
 
-theorem coeFn_injective : Function.Injective (coeFn : Enorm 𝕜 V → V → ℝ≥0∞) := fun e₁ e₂ h => by
+#print ENorm.coeFn_injective /-
+theorem coeFn_injective : Function.Injective (coeFn : ENorm 𝕜 V → V → ℝ≥0∞) := fun e₁ e₂ h => by
   cases e₁ <;> cases e₂ <;> congr <;> exact h
-#align enorm.coe_fn_injective Enorm.coeFn_injective
+#align enorm.coe_fn_injective ENorm.coeFn_injective
+-/
 
 @[ext]
-theorem ext {e₁ e₂ : Enorm 𝕜 V} (h : ∀ x, e₁ x = e₂ x) : e₁ = e₂ :=
+theorem ext {e₁ e₂ : ENorm 𝕜 V} (h : ∀ x, e₁ x = e₂ x) : e₁ = e₂ :=
   coeFn_injective <| funext h
-#align enorm.ext Enorm.ext
+#align enorm.ext ENorm.ext
 
-theorem ext_iff {e₁ e₂ : Enorm 𝕜 V} : e₁ = e₂ ↔ ∀ x, e₁ x = e₂ x :=
+theorem ext_iff {e₁ e₂ : ENorm 𝕜 V} : e₁ = e₂ ↔ ∀ x, e₁ x = e₂ x :=
   ⟨fun h x => h ▸ rfl, ext⟩
-#align enorm.ext_iff Enorm.ext_iff
+#align enorm.ext_iff ENorm.ext_iff
 
 @[simp, norm_cast]
-theorem coe_inj {e₁ e₂ : Enorm 𝕜 V} : (e₁ : V → ℝ≥0∞) = e₂ ↔ e₁ = e₂ :=
+theorem coe_inj {e₁ e₂ : ENorm 𝕜 V} : (e₁ : V → ℝ≥0∞) = e₂ ↔ e₁ = e₂ :=
   coeFn_injective.eq_iff
-#align enorm.coe_inj Enorm.coe_inj
+#align enorm.coe_inj ENorm.coe_inj
 
 @[simp]
 theorem map_smul (c : 𝕜) (x : V) : e (c • x) = ‖c‖₊ * e x :=
@@ -90,49 +94,49 @@ theorem map_smul (c : 𝕜) (x : V) : e (c • x) = ‖c‖₊ * e x :=
       rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top,
           one_mul] <;>
         simp [hc]
-#align enorm.map_smul Enorm.map_smul
+#align enorm.map_smul ENorm.map_smul
 
 @[simp]
 theorem map_zero : e 0 = 0 := by rw [← zero_smul 𝕜 (0 : V), e.map_smul]; norm_num
-#align enorm.map_zero Enorm.map_zero
+#align enorm.map_zero ENorm.map_zero
 
 @[simp]
 theorem eq_zero_iff {x : V} : e x = 0 ↔ x = 0 :=
   ⟨e.eq_zero' x, fun h => h.symm ▸ e.map_zero⟩
-#align enorm.eq_zero_iff Enorm.eq_zero_iff
+#align enorm.eq_zero_iff ENorm.eq_zero_iff
 
 @[simp]
 theorem map_neg (x : V) : e (-x) = e x :=
   calc
     e (-x) = ‖(-1 : 𝕜)‖₊ * e x := by rw [← map_smul, neg_one_smul]
     _ = e x := by simp
 
-#align enorm.map_neg Enorm.map_neg
+#align enorm.map_neg ENorm.map_neg
 
 theorem map_sub_rev (x y : V) : e (x - y) = e (y - x) := by rw [← neg_sub, e.map_neg]
-#align enorm.map_sub_rev Enorm.map_sub_rev
+#align enorm.map_sub_rev ENorm.map_sub_rev
 
 theorem map_add_le (x y : V) : e (x + y) ≤ e x + e y :=
   e.map_add_le' x y
-#align enorm.map_add_le Enorm.map_add_le
+#align enorm.map_add_le ENorm.map_add_le
 
 theorem map_sub_le (x y : V) : e (x - y) ≤ e x + e y :=
   calc
     e (x - y) = e (x + -y) := by rw [sub_eq_add_neg]
     _ ≤ e x + e (-y) := (e.map_add_le x (-y))
     _ = e x + e y := by rw [e.map_neg]
 
-#align enorm.map_sub_le Enorm.map_sub_le
+#align enorm.map_sub_le ENorm.map_sub_le
 
-instance : PartialOrder (Enorm 𝕜 V)
+instance : PartialOrder (ENorm 𝕜 V)
     where
   le e₁ e₂ := ∀ x, e₁ x ≤ e₂ x
   le_refl e x := le_rfl
   le_trans e₁ e₂ e₃ h₁₂ h₂₃ x := le_trans (h₁₂ x) (h₂₃ x)
   le_antisymm e₁ e₂ h₁₂ h₂₁ := ext fun x => le_antisymm (h₁₂ x) (h₂₁ x)
 
 /-- The `enorm` sending each non-zero vector to infinity. -/
-noncomputable instance : Top (Enorm 𝕜 V) :=
+noncomputable instance : Top (ENorm 𝕜 V) :=
   ⟨{  toFun := fun x => if x = 0 then 0 else ⊤
       eq_zero' := fun x => by split_ifs <;> simp [*]
       map_add_le' := fun x y =>
@@ -148,20 +152,20 @@ noncomputable instance : Top (Enorm 𝕜 V) :=
         · tauto
         · simp [hcx.1] }⟩
 
-noncomputable instance : Inhabited (Enorm 𝕜 V) :=
+noncomputable instance : Inhabited (ENorm 𝕜 V) :=
   ⟨⊤⟩
 
-theorem top_map {x : V} (hx : x ≠ 0) : (⊤ : Enorm 𝕜 V) x = ⊤ :=
+theorem top_map {x : V} (hx : x ≠ 0) : (⊤ : ENorm 𝕜 V) x = ⊤ :=
   if_neg hx
-#align enorm.top_map Enorm.top_map
+#align enorm.top_map ENorm.top_map
 
-noncomputable instance : OrderTop (Enorm 𝕜 V)
+noncomputable instance : OrderTop (ENorm 𝕜 V)
     where
   top := ⊤
   le_top e x := if h : x = 0 then by simp [h] else by simp [top_map h]
 
-noncomputable instance : SemilatticeSup (Enorm 𝕜 V) :=
-  { Enorm.partialOrder with
+noncomputable instance : SemilatticeSup (ENorm 𝕜 V) :=
+  { ENorm.partialOrder with
     le := (· ≤ ·)
     lt := (· < ·)
     sup := fun e₁ e₂ =>
@@ -176,15 +180,16 @@ noncomputable instance : SemilatticeSup (Enorm 𝕜 V) :=
     sup_le := fun e₁ e₂ e₃ h₁ h₂ x => max_le (h₁ x) (h₂ x) }
 
 @[simp, norm_cast]
-theorem coe_max (e₁ e₂ : Enorm 𝕜 V) : ⇑(e₁ ⊔ e₂) = fun x => max (e₁ x) (e₂ x) :=
+theorem coe_max (e₁ e₂ : ENorm 𝕜 V) : ⇑(e₁ ⊔ e₂) = fun x => max (e₁ x) (e₂ x) :=
   rfl
-#align enorm.coe_max Enorm.coe_max
+#align enorm.coe_max ENorm.coe_max
 
 @[norm_cast]
-theorem max_map (e₁ e₂ : Enorm 𝕜 V) (x : V) : (e₁ ⊔ e₂) x = max (e₁ x) (e₂ x) :=
+theorem max_map (e₁ e₂ : ENorm 𝕜 V) (x : V) : (e₁ ⊔ e₂) x = max (e₁ x) (e₂ x) :=
   rfl
-#align enorm.max_map Enorm.max_map
+#align enorm.max_map ENorm.max_map
 
+#print ENorm.emetricSpace /-
 /-- Structure of an `emetric_space` defined by an extended norm. -/
 @[reducible]
 def emetricSpace : EMetricSpace V where
@@ -197,8 +202,10 @@ def emetricSpace : EMetricSpace V where
       e (x - z) = e (x - y + (y - z)) := by rw [sub_add_sub_cancel]
       _ ≤ e (x - y) + e (y - z) := e.map_add_le (x - y) (y - z)
       
-#align enorm.emetric_space Enorm.emetricSpace
+#align enorm.emetric_space ENorm.emetricSpace
+-/
 
+#print ENorm.finiteSubspace /-
 /-- The subspace of vectors with finite enorm. -/
 def finiteSubspace : Subspace 𝕜 V where
   carrier := {x | e x < ⊤}
@@ -209,7 +216,8 @@ def finiteSubspace : Subspace 𝕜 V where
       e (c • x) = ‖c‖₊ * e x := e.map_smul c x
       _ < ⊤ := ENNReal.mul_lt_top ENNReal.coe_ne_top hx.Ne
       
-#align enorm.finite_subspace Enorm.finiteSubspace
+#align enorm.finite_subspace ENorm.finiteSubspace
+-/
 
 /-- Metric space structure on `e.finite_subspace`. We use `emetric_space.to_metric_space`
 to ensure that this definition agrees with `e.emetric_space`. -/
@@ -222,11 +230,11 @@ instance : MetricSpace e.finiteSubspace :=
 
 theorem finite_dist_eq (x y : e.finiteSubspace) : dist x y = (e (x - y)).toReal :=
   rfl
-#align enorm.finite_dist_eq Enorm.finite_dist_eq
+#align enorm.finite_dist_eq ENorm.finite_dist_eq
 
 theorem finite_edist_eq (x y : e.finiteSubspace) : edist x y = e (x - y) :=
   rfl
-#align enorm.finite_edist_eq Enorm.finite_edist_eq
+#align enorm.finite_edist_eq ENorm.finite_edist_eq
 
 /-- Normed group instance on `e.finite_subspace`. -/
 instance : NormedAddCommGroup e.finiteSubspace :=
@@ -237,11 +245,11 @@ instance : NormedAddCommGroup e.finiteSubspace :=
 
 theorem finite_norm_eq (x : e.finiteSubspace) : ‖x‖ = (e x).toReal :=
   rfl
-#align enorm.finite_norm_eq Enorm.finite_norm_eq
+#align enorm.finite_norm_eq ENorm.finite_norm_eq
 
 /-- Normed space instance on `e.finite_subspace`. -/
 instance : NormedSpace 𝕜 e.finiteSubspace
     where norm_smul_le c x := le_of_eq <| by simp [finite_norm_eq, ENNReal.toReal_mul]
 
-end Enorm
+end ENorm
 

Mathbin/Analysis/SpecialFunctions/NonIntegrable.lean

@@ -167,6 +167,7 @@ theorem not_intervalIntegrable_of_sub_inv_isBigO_punctured {f : ℝ → F} {a b
       (hf.congr' (A.mono fun x hx => hx.deriv.symm) eventually_eq.rfl) hne hc
 #align not_interval_integrable_of_sub_inv_is_O_punctured not_intervalIntegrable_of_sub_inv_isBigO_punctured
 
+#print intervalIntegrable_sub_inv_iff /-
 /-- The function `λ x, (x - c)⁻¹` is integrable on `a..b` if and only if `a = b` or `c ∉ [a, b]`. -/
 @[simp]
 theorem intervalIntegrable_sub_inv_iff {a b c : ℝ} :
@@ -180,11 +181,14 @@ theorem intervalIntegrable_sub_inv_iff {a b c : ℝ} :
     refine' ((continuous_sub_right c).ContinuousOn.inv₀ _).IntervalIntegrable
     exact fun x hx => sub_ne_zero.2 <| ne_of_mem_of_not_mem hx h₀
 #align interval_integrable_sub_inv_iff intervalIntegrable_sub_inv_iff
+-/
 
+#print intervalIntegrable_inv_iff /-
 /-- The function `λ x, x⁻¹` is integrable on `a..b` if and only if `a = b` or `0 ∉ [a, b]`. -/
 @[simp]
 theorem intervalIntegrable_inv_iff {a b : ℝ} :
     IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ (0 : ℝ) ∉ [a, b] := by
   simp only [← intervalIntegrable_sub_inv_iff, sub_zero]
 #align interval_integrable_inv_iff intervalIntegrable_inv_iff
+-/
 

Mathbin/CategoryTheory/Monoidal/Types/Coyoneda.lean

@@ -31,6 +31,7 @@ open Opposite
 open MonoidalCategory
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+#print CategoryTheory.coyonedaTensorUnit /-
 /-- `(𝟙_ C ⟶ -)` is a lax monoidal functor to `Type`. -/
 def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] :
     LaxMonoidalFunctor C (Type v) :=
@@ -51,6 +52,7 @@ def coyonedaTensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] :
       dsimp; simp only [category.assoc]
       rw [right_unitor_naturality, unitors_inv_equal, iso.inv_hom_id_assoc] }
 #align category_theory.coyoneda_tensor_unit CategoryTheory.coyonedaTensorUnit
+-/
 
 end CategoryTheory
 

Mathbin/MeasureTheory/Covering/BesicovitchVectorSpace.lean

@@ -61,6 +61,7 @@ namespace SatelliteConfig
 
 variable [NormedSpace ℝ E] {N : ℕ} {τ : ℝ} (a : SatelliteConfig E N τ)
 
+#print Besicovitch.SatelliteConfig.centerAndRescale /-
 /-- Rescaling a satellite configuration in a vector space, to put the basepoint at `0` and the base
 radius at `1`. -/
 def centerAndRescale : SatelliteConfig E N τ
@@ -113,6 +114,7 @@ def centerAndRescale : SatelliteConfig E N τ
     convert H using 2
     abel
 #align besicovitch.satellite_config.center_and_rescale Besicovitch.SatelliteConfig.centerAndRescale
+-/
 
 theorem centerAndRescale_center : a.centerAndRescale.c (last N) = 0 := by
   simp [satellite_config.center_and_rescale]
@@ -128,11 +130,13 @@ end SatelliteConfig
 /-! ### Disjoint balls of radius close to `1` in the radius `2` ball. -/
 
 
+#print Besicovitch.multiplicity /-
 /-- The maximum cardinality of a `1`-separated set in the ball of radius `2`. This is also the
 optimal number of families in the Besicovitch covering theorem. -/
 def multiplicity (E : Type _) [NormedAddCommGroup E] :=
   sSup {N | ∃ s : Finset E, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}
 #align besicovitch.multiplicity Besicovitch.multiplicity
+-/
 
 section
 
@@ -190,13 +194,15 @@ theorem card_le_of_separated (s : Finset E) (hs : ∀ c ∈ s, ‖c‖ ≤ 2)
   exact_mod_cast K
 #align besicovitch.card_le_of_separated Besicovitch.card_le_of_separated
 
+#print Besicovitch.multiplicity_le /-
 theorem multiplicity_le : multiplicity E ≤ 5 ^ finrank ℝ E :=
   by
   apply csSup_le
   · refine' ⟨0, ⟨∅, by simp⟩⟩
   · rintro _ ⟨s, ⟨rfl, h⟩⟩
     exact Besicovitch.card_le_of_separated s h.1 h.2
 #align besicovitch.multiplicity_le Besicovitch.multiplicity_le
+-/
 
 theorem card_le_multiplicity {s : Finset E} (hs : ∀ c ∈ s, ‖c‖ ≤ 2)
     (h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) : s.card ≤ multiplicity E :=
@@ -213,7 +219,7 @@ variable (E)
 
 /-- If `δ` is small enough, a `(1-δ)`-separated set in the ball of radius `2` also has cardinality
 at most `multiplicity E`. -/
-theorem exists_good_δ :
+theorem exists_goodδ :
     ∃ δ : ℝ,
       0 < δ ∧
         δ < 1 ∧
@@ -297,24 +303,28 @@ theorem exists_good_δ :
   have : s.card ≤ multiplicity E := card_le_multiplicity hs h's
   rw [s_card, hN] at this 
   exact lt_irrefl _ ((Nat.lt_succ_self (multiplicity E)).trans_le this)
-#align besicovitch.exists_good_δ Besicovitch.exists_good_δ
+#align besicovitch.exists_good_δ Besicovitch.exists_goodδ
 
+#print Besicovitch.goodδ /-
 /-- A small positive number such that any `1 - δ`-separated set in the ball of radius `2` has
 cardinality at most `besicovitch.multiplicity E`. -/
 def goodδ : ℝ :=
-  (exists_good_δ E).some
+  (exists_goodδ E).some
 #align besicovitch.good_δ Besicovitch.goodδ
+-/
 
 theorem goodδ_lt_one : goodδ E < 1 :=
-  (exists_good_δ E).choose_spec.2.1
+  (exists_goodδ E).choose_spec.2.1
 #align besicovitch.good_δ_lt_one Besicovitch.goodδ_lt_one
 
+#print Besicovitch.goodτ /-
 /-- A number `τ > 1`, but chosen close enough to `1` so that the construction in the Besicovitch
 covering theorem using this parameter `τ` will give the smallest possible number of covering
 families. -/
 def goodτ : ℝ :=
   1 + goodδ E / 4
 #align besicovitch.good_τ Besicovitch.goodτ
+-/
 
 theorem one_lt_goodτ : 1 < goodτ E := by dsimp [good_τ, good_δ];
   linarith [(exists_good_δ E).choose_spec.1]
@@ -324,7 +334,7 @@ variable {E}
 
 theorem card_le_multiplicity_of_δ {s : Finset E} (hs : ∀ c ∈ s, ‖c‖ ≤ 2)
     (h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖) : s.card ≤ multiplicity E :=
-  (Classical.choose_spec (exists_good_δ E)).2.2 s hs h's
+  (Classical.choose_spec (exists_goodδ E)).2.2 s hs h's
 #align besicovitch.card_le_multiplicity_of_δ Besicovitch.card_le_multiplicity_of_δ
 
 theorem le_multiplicity_of_δ_of_fin {n : ℕ} (f : Fin n → E) (h : ∀ i, ‖f i‖ ≤ 2)
@@ -576,6 +586,7 @@ end SatelliteConfig
 
 variable (E) [NormedSpace ℝ E] [FiniteDimensional ℝ E]
 
+#print Besicovitch.isEmpty_satelliteConfig_multiplicity /-
 /-- In a normed vector space `E`, there can be no satellite configuration with `multiplicity E + 1`
 points and the parameter `good_τ E`. This will ensure that in the inductive construction to get
 the Besicovitch covering families, there will never be more than `multiplicity E` nonempty
@@ -591,6 +602,7 @@ theorem isEmpty_satelliteConfig_multiplicity :
     exact
       lt_irrefl _ ((Nat.lt_succ_self _).trans_le (le_multiplicity_of_δ_of_fin c' c'_le_two hc'))⟩
 #align besicovitch.is_empty_satellite_config_multiplicity Besicovitch.isEmpty_satelliteConfig_multiplicity
+-/
 
 instance (priority := 100) : HasBesicovitchCovering E :=
   ⟨⟨multiplicity E, goodτ E, one_lt_goodτ E, isEmpty_satelliteConfig_multiplicity E⟩⟩