Fix linter option names and the warnings they expose

StatsMLlib/Analysis/MetricEntropy/Basic.lean

@@ -52,7 +52,8 @@ lemma metricEntropyOfNat_nonneg (n : ℕ) : 0 ≤ metricEntropyOfNat n := by
   · push Not at hn
     exact Real.log_nonneg (Nat.one_le_cast.mpr (Nat.one_le_of_lt hn))
 
-lemma metricEntropyOfNat_mono {n m : ℕ} (h : n ≤ m) : metricEntropyOfNat n ≤ metricEntropyOfNat m := by
+lemma metricEntropyOfNat_mono {n m : ℕ} (h : n ≤ m) :
+    metricEntropyOfNat n ≤ metricEntropyOfNat m := by
   unfold metricEntropyOfNat
   split_ifs with hn hm hm
   · exact le_rfl
@@ -296,7 +297,8 @@ lemma sqrt_log_card_le_sqrtEntropy_of_card_le {eps : ℝ} {s : Set A} {n : ℕ}
           interval_cases n
           · simp
           · simp
-        have hlog_m : 0 ≤ Real.log (m : ℝ) := Real.log_nonneg (Nat.one_le_cast.mpr (by omega : 1 ≤ m))
+        have hlog_m : 0 ≤ Real.log (m : ℝ) :=
+          Real.log_nonneg (Nat.one_le_cast.mpr (by omega : 1 ≤ m))
         linarith
       · -- n > 1: use log monotonicity
         push Not at hn1
@@ -331,11 +333,13 @@ lemma sqrt_log_mul_le {a b : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b) :
     have hsq_a : Real.sqrt (Real.log (a : ℝ))^2 = Real.log (a : ℝ) := Real.sq_sqrt hlog_a_nonneg
     have hsq_b : Real.sqrt (Real.log (b : ℝ))^2 = Real.log (b : ℝ) := Real.sq_sqrt hlog_b_nonneg
     have hsq : (Real.sqrt (Real.log (a : ℝ)) + Real.sqrt (Real.log (b : ℝ)))^2 =
-        Real.log (a : ℝ) + 2 * Real.sqrt (Real.log (a : ℝ)) * Real.sqrt (Real.log (b : ℝ)) + Real.log (b : ℝ) := by
+        Real.log (a : ℝ) + 2 * Real.sqrt (Real.log (a : ℝ)) * Real.sqrt (Real.log (b : ℝ)) +
+          Real.log (b : ℝ) := by
       ring_nf
       rw [hsq_a, hsq_b]
     rw [hsq]
-    have h_cross_nonneg : 0 ≤ 2 * Real.sqrt (Real.log (a : ℝ)) * Real.sqrt (Real.log (b : ℝ)) := by positivity
+    have h_cross_nonneg :
+        0 ≤ 2 * Real.sqrt (Real.log (a : ℝ)) * Real.sqrt (Real.log (b : ℝ)) := by positivity
     linarith
   calc Real.sqrt (Real.log (a : ℝ) + Real.log (b : ℝ))
     _ ≤ Real.sqrt ((Real.sqrt (Real.log a) + Real.sqrt (Real.log b))^2) := Real.sqrt_le_sqrt key
@@ -859,7 +863,8 @@ lemma entropyIntegralENNRealTrunc_le_dyadic_sum_strong
       have hhalf_le_D : D / 2 ≤ D := by linarith
       have hhalf_pos : 0 < D / 2 := by linarith
       -- Split the integral
-      -- Note: goal has `let δ := D * 2 ^ (-↑(n' + 1 + 1))` which equals our local δ = D * 2 ^ (-↑(n' + 2))
+      -- Note: goal has `let δ := D * 2 ^ (-↑(n' + 1 + 1))` which equals our local
+      -- δ = D * 2 ^ (-↑(n' + 2))
       -- n' + 1 + 1 = n' + 2 definitionally, so we can just intro and use the split directly
       intro δ'
       have hδ'_eq : δ' = δ := rfl

StatsMLlib/Analysis/MetricEntropy/Chaining.lean

@@ -70,15 +70,16 @@ theorem exists_dyadicNets {s : Set A} (hs : TotallyBounded s) {D : ℝ} (hD : 0
 /-- DyadicNets with cardinality bounds: each net at scale k has cardinality bounded by
     the covering number at the next finer scale (k+1). This bound is crucial for relating
     chaining arguments to covering numbers in Dudley's theorem. -/
-structure GoodDyadicNets (s : Set A) (D : ℝ) (hD : 0 < D) (hs : TotallyBounded s) extends DyadicNets s D where
+structure GoodDyadicNets (s : Set A) (D : ℝ) (hD : 0 < D) (hs : TotallyBounded s)
+    extends DyadicNets s D where
   /-- Each net at scale k has cardinality ≤ coveringNumber at scale k+1 -/
   card_bound : ∀ k, (nets k).card ≤ (coveringNumber (dyadicScale D (k + 1)) s).untop
       (ne_top_of_lt (coveringNumber_lt_top_of_totallyBounded (dyadicScale_pos hD (k + 1)) hs))
 
 /-- Good dyadic nets exist for nonempty totally bounded sets.
     The key insight: use exists_enet_subset_from_half at each scale, which gives an eps-net
-    inside s with cardinality ≤ coveringNumber(eps/2). Since dyadicScale D k / 2 = dyadicScale D (k+1),
-    this gives the desired cardinality bound. -/
+    inside s with cardinality ≤ coveringNumber(eps/2). Since
+    dyadicScale D k / 2 = dyadicScale D (k+1), this gives the desired cardinality bound. -/
 theorem exists_goodDyadicNets {s : Set A} (hs : TotallyBounded s) (hsne : s.Nonempty)
     {D : ℝ} (hD : 0 < D) :
     Nonempty (GoodDyadicNets s D hD hs) := by
@@ -116,7 +117,8 @@ lemma exists_near_in_net {t : Finset A} {eps : ℝ} {s : Set A}
 
 /-- The chaining approximation: for any point x and any level K,
     there exists a sequence of approximations through the nets. -/
-theorem chaining_approximation {s : Set A} {D : ℝ} (dn : DyadicNets s D) {x : A} (hx : x ∈ s) (K : ℕ) :
+theorem chaining_approximation {s : Set A} {D : ℝ} (dn : DyadicNets s D) {x : A} (hx : x ∈ s)
+    (K : ℕ) :
     ∃ y ∈ dn.nets K, dist x y ≤ dyadicScale D K :=
   exists_near_in_net (dn.isNet K) hx
 

StatsMLlib/Analysis/NormedSpace/CoveringNumber/Euclidean.lean

@@ -36,12 +36,14 @@ abbrev euclideanBall (R : ℝ) : Set (EuclideanSpace ℝ ι) := Metric.closedBal
 
 omit [Nonempty ι] in
 /-- The Euclidean ball is totally bounded (since it's compact in finite dimensions). -/
-lemma euclideanBall_totallyBounded (R : ℝ) : TotallyBounded (euclideanBall R : Set (EuclideanSpace ℝ ι)) :=
+lemma euclideanBall_totallyBounded (R : ℝ) :
+    TotallyBounded (euclideanBall R : Set (EuclideanSpace ℝ ι)) :=
   (ProperSpace.isCompact_closedBall 0 R).totallyBounded
 
 omit [Nonempty ι] in
 /-- The Euclidean ball is nonempty for non-negative radius. -/
-lemma euclideanBall_nonempty {R : ℝ} (hR : 0 ≤ R) : (euclideanBall R : Set (EuclideanSpace ℝ ι)).Nonempty :=
+lemma euclideanBall_nonempty {R : ℝ} (hR : 0 ≤ R) :
+    (euclideanBall R : Set (EuclideanSpace ℝ ι)).Nonempty :=
   ⟨0, Metric.mem_closedBall_self hR⟩
 
 /-- If points x and y are ε-separated (dist x y > ε), then the closed balls of radius ε/2
@@ -62,7 +64,8 @@ lemma packing_halfBalls_pairwiseDisjoint {E : Type*} [PseudoMetricSpace E]
   have hsep := hpacking.2 hx hy hxy
   exact closedBall_half_disjoint heps hsep
 
-/-- A half-radius ball around a point in closedBall(0, R) is contained in closedBall(0, R + eps/2). -/
+/-- A half-radius ball around a point in closedBall(0, R) is contained in
+closedBall(0, R + eps/2). -/
 lemma halfBall_subset_enlargedBall {E : Type*} [SeminormedAddCommGroup E]
     {x : E} {R eps : ℝ} (hx : x ∈ Metric.closedBall (0 : E) R) :
     Metric.closedBall x (eps / 2) ⊆ Metric.closedBall (0 : E) (R + eps / 2) := by
@@ -162,12 +165,14 @@ lemma packing_card_bound_aux
       ENNReal.ofReal ((eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) :=
     fun x => volume_closedBall_eq_rpow x (eps / 2) heps_half_nonneg
   -- Volume of large ball
-  have hvol_large : MeasureTheory.volume (Metric.closedBall (0 : EuclideanSpace ℝ ι) (R + eps / 2)) =
+  have hvol_large :
+      MeasureTheory.volume (Metric.closedBall (0 : EuclideanSpace ℝ ι) (R + eps / 2)) =
       ENNReal.ofReal ((R + eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) :=
     volume_closedBall_eq_rpow 0 (R + eps / 2) hR_plus_pos
   -- Sum of small ball volumes
   have hvol_sum : ∑ x ∈ t, MeasureTheory.volume (Metric.closedBall x (eps / 2)) =
-      t.card * ENNReal.ofReal ((eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) := by
+      t.card * ENNReal.ofReal
+        ((eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) := by
     simp only [hvol_small]
     rw [sum_const]
     simp only [nsmul_eq_mul]
@@ -178,13 +183,18 @@ lemma packing_card_bound_aux
   have hconst_pos := euclideanBallVolumeConst_pos (Fintype.card ι)
   have hsmall_pos : 0 < (eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) :=
     mul_pos (pow_pos heps_half_pos _) hconst_pos
-  have hlarge_pos : 0 < (R + eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) :=
+  have hlarge_pos :
+      0 < (R + eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) :=
     mul_pos (pow_pos (by linarith : 0 < R + eps / 2) _) hconst_pos
-  have hlarge_nonneg : 0 ≤ (R + eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) :=
+  have hlarge_nonneg :
+      0 ≤ (R + eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) :=
     le_of_lt hlarge_pos
   -- Use ENNReal.ofReal for the bound
-  have h : t.card * ENNReal.ofReal ((eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) ≤
-      ENNReal.ofReal ((R + eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) := hvol_le
+  have h :
+      t.card * ENNReal.ofReal
+        ((eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) ≤
+      ENNReal.ofReal ((R + eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) :=
+    hvol_le
   rw [← ENNReal.ofReal_natCast] at h
   rw [← ENNReal.ofReal_mul (Nat.cast_nonneg _)] at h
   have h' := ENNReal.ofReal_le_ofReal_iff hlarge_nonneg |>.mp h
@@ -194,7 +204,8 @@ lemma packing_card_bound_aux
   have hcancel : (t.card : ℝ) ≤ (R + eps / 2) ^ Fintype.card ι / (eps / 2) ^ Fintype.card ι := by
     have hne : (eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) ≠ 0 :=
       ne_of_gt hsmall_pos
-    have hsmall_nonneg : 0 ≤ (eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) :=
+    have hsmall_nonneg :
+        0 ≤ (eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι) :=
       le_of_lt hsmall_pos
     calc (t.card : ℝ)
       _ = t.card * ((eps / 2) ^ Fintype.card ι * euclideanBallVolumeConst (Fintype.card ι)) /
@@ -241,7 +252,8 @@ lemma separated_finite_of_totallyBounded {E : Type*} [PseudoMetricSpace E]
     t.Finite := by
   -- If s is covered by finitely many ε/2-balls, any ε-separated set has bounded cardinality
   have heps2 : 0 < eps / 2 := by linarith
-  obtain ⟨cover, _, hcover_finite, hcover⟩ := Metric.finite_approx_of_totallyBounded hs (eps / 2) heps2
+  obtain ⟨cover, _, hcover_finite, hcover⟩ :=
+    Metric.finite_approx_of_totallyBounded hs (eps / 2) heps2
   -- Each ε/2-ball can contain at most one point from t
   -- Define a function from t to cover: for each x ∈ t, pick a c ∈ cover with x ∈ ball(c, eps/2)
   classical
@@ -265,7 +277,8 @@ lemma separated_finite_of_totallyBounded {E : Type*} [PseudoMetricSpace E]
       have hsep_xy := ht_sep hx hy hxy
       have hdist : dist x y < eps := by
         have heq' : (hmaps x hx).choose = (hmaps y hy).choose := heq
-        calc dist x y ≤ dist x (hmaps x hx).choose + dist (hmaps x hx).choose y := dist_triangle _ _ _
+        calc dist x y ≤ dist x (hmaps x hx).choose + dist (hmaps x hx).choose y :=
+            dist_triangle _ _ _
           _ < eps / 2 + eps / 2 := by
             apply add_lt_add
             · exact Metric.mem_ball.mp hxc
@@ -285,7 +298,8 @@ lemma exists_maximal_packing {E : Type*} [PseudoMetricSpace E]
   classical
   -- Get the cover that bounds packing sizes
   have heps2 : 0 < eps / 2 := by linarith
-  obtain ⟨cover, _, hcover_finite, hcover⟩ := Metric.finite_approx_of_totallyBounded hs (eps / 2) heps2
+  obtain ⟨cover, _, hcover_finite, hcover⟩ :=
+    Metric.finite_approx_of_totallyBounded hs (eps / 2) heps2
   -- Any packing has size at most |cover|
   have hbound : ∀ t : Finset E, IsPacking t eps s → t.card ≤ cover.ncard := by
     intro t ht
@@ -308,7 +322,8 @@ lemma exists_maximal_packing {E : Type*} [PseudoMetricSpace E]
         have hsep_xy := ht_sep hx hy hxy
         have heq' : (hmaps x hx).choose = (hmaps y hy).choose := heq
         have hdist : dist x y < eps := by
-          calc dist x y ≤ dist x (hmaps x hx).choose + dist (hmaps x hx).choose y := dist_triangle _ _ _
+          calc dist x y ≤ dist x (hmaps x hx).choose + dist (hmaps x hx).choose y :=
+              dist_triangle _ _ _
             _ < eps / 2 + eps / 2 := by
               apply add_lt_add
               · exact Metric.mem_ball.mp hxc