Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit d003c55

Browse files
YaelDilliesYaelDillies
committed
chore(analysis, measure_theory): Fix lint (#16216)
Satisfy the `fintype_finite` and `to_additive_doc` linters. Further, perform the similar weakening from `encodable` to `countable`, even though that's not yet linted for. The advantage of this is that `finite α → countable α` in known to TC inference, while `fintype α → encodable α` is not (because it's noncanonical data). As a result, some lemmas that were proved for both `fintype` and `encodable` are now deduplicated.
1 parent 3d7987c commit d003c55

78 files changed

Lines changed: 412 additions & 445 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎src/analysis/box_integral/box/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -335,7 +335,7 @@ lemma Ioo_subset_coe (I : box ι) : I.Ioo ⊆ I := λ x hx i, Ioo_subset_Ioc_sel
335335

336336
protected lemma Ioo_subset_Icc (I : box ι) : I.Ioo ⊆ I.Icc := I.Ioo_subset_coe.trans coe_subset_Icc
337337

338-
lemma Union_Ioo_of_tendsto [fintype ι] {I : box ι} {J : ℕ → box ι} (hJ : monotone J)
338+
lemma Union_Ioo_of_tendsto [finite ι] {I : box ι} {J : ℕ → box ι} (hJ : monotone J)
339339
(hl : tendsto (lower ∘ J) at_top (𝓝 I.lower)) (hu : tendsto (upper ∘ J) at_top (𝓝 I.upper)) :
340340
(⋃ n, (J n).Ioo) = I.Ioo :=
341341
have hl' : ∀ i, antitone (λ n, (J n).lower i),

‎src/analysis/box_integral/integrability.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ begin
102102
measure less than `ε / 2 ^ n / (n + 1)`. Then the norm of the integral sum is less than `ε`. -/
103103
refine has_integral_iff.2 (λ ε ε0, _),
104104
lift ε to ℝ≥0 using ε0.lt.le, rw [gt_iff_lt, nnreal.coe_pos] at ε0,
105-
rcases nnreal.exists_pos_sum_of_encodable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩,
105+
rcases nnreal.exists_pos_sum_of_countable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩,
106106
haveI := fact.mk (I.measure_coe_lt_top μ),
107107
change μ.restrict I {x | f x ≠ 0} = 0 at hf,
108108
set N : (ι → ℝ) → ℕ := λ x, ⌈∥f x∥⌉₊,
@@ -237,7 +237,7 @@ begin
237237
exact ((eventually_ge_at_top N₀).and $ this $ closed_ball_mem_nhds _ ε0).exists },
238238
choose Nx hNx hNxε,
239239
/- We also choose a convergent series with `∑' i : ℕ, δ i < ε`. -/
240-
rcases nnreal.exists_pos_sum_of_encodable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩,
240+
rcases nnreal.exists_pos_sum_of_countable ε0.ne' ℕ with ⟨δ, δ0, c, hδc, hcε⟩,
241241
/- Since each simple function `fᵢ` is integrable, there exists `rᵢ : ℝⁿ → (0, ∞)` such that
242242
the integral sum of `f` over any tagged prepartition is `δᵢ`-close to the sum of integrals
243243
of `fᵢ` over the boxes of this prepartition. For each `x`, we choose `r (Nx x)` as the radius

‎src/analysis/box_integral/partition/additive.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ map. -/
134134

135135
/-- If `f` is a box additive function on subboxes of `I` and `π₁`, `π₂` are two prepartitions of
136136
`I` that cover the same part of `I`, then `∑ J in π₁.boxes, f J = ∑ J in π₂.boxes, f J`. -/
137-
lemma sum_boxes_congr [fintype ι] (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) {π₁ π₂ : prepartition I}
137+
lemma sum_boxes_congr [finite ι] (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) {π₁ π₂ : prepartition I}
138138
(h : π₁.Union = π₂.Union) :
139139
∑ J in π₁.boxes, f J = ∑ J in π₂.boxes, f J :=
140140
begin

‎src/analysis/box_integral/partition/measure.lean‎

Lines changed: 12 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -34,28 +34,27 @@ namespace box_integral
3434
open measure_theory
3535

3636
namespace box
37+
variables (I : box ι)
3738

38-
lemma measure_Icc_lt_top (I : box ι) (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] :
39-
μ I.Icc < ∞ :=
39+
lemma measure_Icc_lt_top (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] : μ I.Icc < ∞ :=
4040
show μ (Icc I.lower I.upper) < ∞, from I.is_compact_Icc.measure_lt_top
4141

42-
lemma measure_coe_lt_top (I : box ι) (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] :
43-
μ I < ∞ :=
42+
lemma measure_coe_lt_top (μ : measure (ι → ℝ)) [is_locally_finite_measure μ] : μ I < ∞ :=
4443
(measure_mono $ coe_subset_Icc).trans_lt (I.measure_Icc_lt_top μ)
4544

46-
variables [fintype ι] (I : box ι)
45+
section countable
46+
variables [countable ι]
4747

4848
lemma measurable_set_coe : measurable_set (I : set (ι → ℝ)) :=
49-
begin
50-
rw [coe_eq_pi],
51-
haveI := fintype.to_encodable ι,
52-
exact measurable_set.univ_pi (λ i, measurable_set_Ioc)
53-
end
49+
by { rw coe_eq_pi, exact measurable_set.univ_pi (λ i, measurable_set_Ioc) }
5450

5551
lemma measurable_set_Icc : measurable_set I.Icc := measurable_set_Icc
5652

57-
lemma measurable_set_Ioo : measurable_set I.Ioo :=
58-
(measurable_set_pi (set.to_finite _).countable).2 $ or.inl $ λ i hi, measurable_set_Ioo
53+
lemma measurable_set_Ioo : measurable_set I.Ioo := measurable_set.univ_pi $ λ i, measurable_set_Ioo
54+
55+
end countable
56+
57+
variables [fintype ι]
5958

6059
lemma coe_ae_eq_Icc : (I : set (ι → ℝ)) =ᵐ[volume] I.Icc :=
6160
by { rw coe_eq_pi, exact measure.univ_pi_Ioc_ae_eq_Icc }
@@ -65,7 +64,7 @@ measure.univ_pi_Ioo_ae_eq_Icc
6564

6665
end box
6766

68-
lemma prepartition.measure_Union_to_real [fintype ι] {I : box ι} (π : prepartition I)
67+
lemma prepartition.measure_Union_to_real [finite ι] {I : box ι} (π : prepartition I)
6968
(μ : measure (ι → ℝ)) [is_locally_finite_measure μ] :
7069
(μ π.Union).to_real = ∑ J in π.boxes, (μ J).to_real :=
7170
begin

‎src/analysis/box_integral/partition/split.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -258,7 +258,7 @@ end
258258

259259
section fintype
260260

261-
variable [fintype ι]
261+
variable [finite ι]
262262

263263
/-- Let `s` be a finite set of boxes in `ℝⁿ = ι → ℝ`. Then there exists a finite set `t₀` of
264264
hyperplanes (namely, the set of all hyperfaces of boxes in `s`) such that for any `t ⊇ t₀`
@@ -269,6 +269,7 @@ lemma eventually_not_disjoint_imp_le_of_mem_split_many (s : finset (box ι)) :
269269
∀ᶠ t : finset (ι × ℝ) in at_top, ∀ (I : box ι) (J ∈ s) (J' ∈ split_many I t),
270270
¬disjoint (J : with_bot (box ι)) J' → J' ≤ J :=
271271
begin
272+
casesI nonempty_fintype ι,
272273
refine eventually_at_top.2
273274
⟨s.bUnion (λ J, finset.univ.bUnion (λ i, {(i, J.lower i), (i, J.upper i)})),
274275
λ t ht I J hJ J' hJ', not_disjoint_imp_le_of_subset_of_mem_split_many (λ i, _) hJ'⟩,

‎src/analysis/calculus/fderiv_measurable.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -378,8 +378,8 @@ is Borel-measurable. -/
378378
theorem measurable_set_of_differentiable_at_of_is_complete
379379
{K : set (E →L[𝕜] F)} (hK : is_complete K) :
380380
measurable_set {x | differentiable_at 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} :=
381-
by simp [differentiable_set_eq_D K hK, D, is_open_B.measurable_set, measurable_set.Inter_Prop,
382-
measurable_set.Inter, measurable_set.Union]
381+
by simp [differentiable_set_eq_D K hK, D, is_open_B.measurable_set, measurable_set.Inter,
382+
measurable_set.Union]
383383

384384
variable [complete_space F]
385385

@@ -728,8 +728,8 @@ set, is Borel-measurable. -/
728728
theorem measurable_set_of_differentiable_within_at_Ici_of_is_complete
729729
{K : set F} (hK : is_complete K) :
730730
measurable_set {x | differentiable_within_at ℝ f (Ici x) x ∧ deriv_within f (Ici x) x ∈ K} :=
731-
by simp [differentiable_set_eq_D K hK, D, measurable_set_B, measurable_set.Inter_Prop,
732-
measurable_set.Inter, measurable_set.Union]
731+
by simp [differentiable_set_eq_D K hK, D, measurable_set_B, measurable_set.Inter,
732+
measurable_set.Union]
733733

734734
variable [complete_space F]
735735

‎src/analysis/calculus/lagrange_multipliers.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -133,13 +133,14 @@ Then the derivatives `f' i : E → L[ℝ] ℝ` and `φ' : E →L[ℝ] ℝ` are l
133133
See also `is_local_extr_on.exists_multipliers_of_has_strict_fderiv_at` for a version that
134134
that states existence of Lagrange multipliers `Λ` and `Λ₀` instead of using
135135
`¬linear_independent ℝ _` -/
136-
lemma is_local_extr_on.linear_dependent_of_has_strict_fderiv_at {ι : Type*} [fintype ι]
136+
lemma is_local_extr_on.linear_dependent_of_has_strict_fderiv_at {ι : Type*} [finite ι]
137137
{f : ι → E → ℝ} {f' : ι → E →L[ℝ] ℝ}
138138
(hextr : is_local_extr_on φ {x | ∀ i, f i x = f i x₀} x₀)
139139
(hf' : ∀ i, has_strict_fderiv_at (f i) (f' i) x₀)
140140
(hφ' : has_strict_fderiv_at φ φ' x₀) :
141141
¬linear_independent ℝ (option.elim φ' f' : option ι → E →L[ℝ] ℝ) :=
142142
begin
143+
casesI nonempty_fintype ι,
143144
rw [fintype.linear_independent_iff], push_neg,
144145
rcases hextr.exists_multipliers_of_has_strict_fderiv_at hf' hφ' with ⟨Λ, Λ₀, hΛ, hΛf⟩,
145146
refine ⟨option.elim Λ₀ Λ, _, _⟩,

‎src/analysis/calculus/tangent_cone.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -324,7 +324,7 @@ begin
324324
exact (hs.1.prod ht.1).mono this
325325
end
326326

327-
lemma unique_diff_within_at.univ_pi (ι : Type*) [fintype ι] (E : ι → Type*)
327+
lemma unique_diff_within_at.univ_pi (ι : Type*) [finite ι] (E : ι → Type*)
328328
[Π i, normed_add_comm_group (E i)] [Π i, normed_space 𝕜 (E i)]
329329
(s : Π i, set (E i)) (x : Π i, E i) (h : ∀ i, unique_diff_within_at 𝕜 (s i) (x i)) :
330330
unique_diff_within_at 𝕜 (set.pi univ s) x :=
@@ -338,7 +338,7 @@ begin
338338
exact λ i, (maps_to_tangent_cone_pi $ λ j hj, (h j).2).mono subset.rfl submodule.subset_span
339339
end
340340

341-
lemma unique_diff_within_at.pi (ι : Type*) [fintype ι] (E : ι → Type*)
341+
lemma unique_diff_within_at.pi (ι : Type*) [finite ι] (E : ι → Type*)
342342
[Π i, normed_add_comm_group (E i)] [Π i, normed_space 𝕜 (E i)]
343343
(s : Π i, set (E i)) (x : Π i, E i) (I : set ι)
344344
(h : ∀ i ∈ I, unique_diff_within_at 𝕜 (s i) (x i)) :
@@ -357,15 +357,15 @@ lemma unique_diff_on.prod {t : set F} (hs : unique_diff_on 𝕜 s) (ht : unique_
357357

358358
/-- The finite product of a family of sets of unique differentiability is a set of unique
359359
differentiability. -/
360-
lemma unique_diff_on.pi (ι : Type*) [fintype ι] (E : ι → Type*)
360+
lemma unique_diff_on.pi (ι : Type*) [finite ι] (E : ι → Type*)
361361
[Π i, normed_add_comm_group (E i)] [Π i, normed_space 𝕜 (E i)]
362362
(s : Π i, set (E i)) (I : set ι) (h : ∀ i ∈ I, unique_diff_on 𝕜 (s i)) :
363363
unique_diff_on 𝕜 (set.pi I s) :=
364364
λ x hx, unique_diff_within_at.pi _ _ _ _ _ $ λ i hi, h i hi (x i) (hx i hi)
365365

366366
/-- The finite product of a family of sets of unique differentiability is a set of unique
367367
differentiability. -/
368-
lemma unique_diff_on.univ_pi (ι : Type*) [fintype ι] (E : ι → Type*)
368+
lemma unique_diff_on.univ_pi (ι : Type*) [finite ι] (E : ι → Type*)
369369
[Π i, normed_add_comm_group (E i)] [Π i, normed_space 𝕜 (E i)]
370370
(s : Π i, set (E i)) (h : ∀ i, unique_diff_on 𝕜 (s i)) :
371371
unique_diff_on 𝕜 (set.pi univ s) :=

‎src/analysis/normed_space/add_torsor_bases.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ to this basis.
5454
5555
TODO Restate this result for affine spaces (instead of vector spaces) once the definition of
5656
convexity is generalised to this setting. -/
57-
lemma interior_convex_hull_aff_basis {ι E : Type*} [fintype ι] [normed_add_comm_group E]
57+
lemma interior_convex_hull_aff_basis {ι E : Type*} [finite ι] [normed_add_comm_group E]
5858
[normed_space ℝ E] (b : affine_basis ι ℝ E) :
5959
interior (convex_hull ℝ (range b.points)) = { x | ∀ i, 0 < b.coord i x } :=
6060
begin

‎src/analysis/normed_space/finite_dimension.lean‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ begin
154154
change continuous (λ (f : E →L[𝕜] E), (f : E →ₗ[𝕜] E).det),
155155
by_cases h : ∃ (s : finset E), nonempty (basis ↥s 𝕜 E),
156156
{ rcases h with ⟨s, ⟨b⟩⟩,
157-
haveI : finite_dimensional 𝕜 E := finite_dimensional.of_finset_basis b,
157+
haveI : finite_dimensional 𝕜 E := finite_dimensional.of_fintype_basis b,
158158
simp_rw linear_map.det_eq_det_to_matrix_of_finset b,
159159
refine continuous.matrix_det _,
160160
exact ((linear_map.to_matrix b b).to_linear_map.comp
@@ -216,9 +216,10 @@ begin
216216
exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩ }
217217
end
218218

219-
protected lemma linear_independent.eventually {ι} [fintype ι] {f : ι → E}
219+
protected lemma linear_independent.eventually {ι} [finite ι] {f : ι → E}
220220
(hf : linear_independent 𝕜 f) : ∀ᶠ g in 𝓝 f, linear_independent 𝕜 g :=
221221
begin
222+
casesI nonempty_fintype ι,
222223
simp only [fintype.linear_independent_iff'] at hf ⊢,
223224
rcases linear_map.exists_antilipschitz_with _ hf with ⟨K, K0, hK⟩,
224225
have : tendsto (λ g : ι → E, ∑ i, ∥g i - f i∥) (𝓝 f) (𝓝 $ ∑ i, ∥f i - f i∥),
@@ -237,7 +238,7 @@ begin
237238
exact mul_le_mul_of_nonneg_left (norm_le_pi_norm (v - u) i) (norm_nonneg _)
238239
end
239240

240-
lemma is_open_set_of_linear_independent {ι : Type*} [fintype ι] :
241+
lemma is_open_set_of_linear_independent {ι : Type*} [finite ι] :
241242
is_open {f : ι → E | linear_independent 𝕜 f} :=
242243
is_open_iff_mem_nhds.2 $ λ f, linear_independent.eventually
243244

@@ -331,14 +332,15 @@ lemma basis.op_norm_le {ι : Type*} [fintype ι] (v : basis ι 𝕜 E) {u : E
331332
by simpa using nnreal.coe_le_coe.mpr (v.op_nnnorm_le ⟨M, hM⟩ hu)
332333

333334
/-- A weaker version of `basis.op_nnnorm_le` that abstracts away the value of `C`. -/
334-
lemma basis.exists_op_nnnorm_le {ι : Type*} [fintype ι] (v : basis ι 𝕜 E) :
335+
lemma basis.exists_op_nnnorm_le {ι : Type*} [finite ι] (v : basis ι 𝕜 E) :
335336
∃ C > (0 : ℝ≥0), ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ i, ∥u (v i)∥₊ ≤ M) → ∥u∥₊ ≤ C*M :=
336-
⟨ max (fintype.card ι • ∥v.equiv_funL.to_continuous_linear_map∥₊) 1,
337+
by casesI nonempty_fintype ι; exact
338+
⟨max (fintype.card ι • ∥v.equiv_funL.to_continuous_linear_map∥₊) 1,
337339
zero_lt_one.trans_le (le_max_right _ _),
338340
λ u M hu, (v.op_nnnorm_le M hu).trans $ mul_le_mul_of_nonneg_right (le_max_left _ _) (zero_le M)⟩
339341

340342
/-- A weaker version of `basis.op_norm_le` that abstracts away the value of `C`. -/
341-
lemma basis.exists_op_norm_le {ι : Type*} [fintype ι] (v : basis ι 𝕜 E) :
343+
lemma basis.exists_op_norm_le {ι : Type*} [finite ι] (v : basis ι 𝕜 E) :
342344
∃ C > (0 : ℝ), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥u (v i)∥ ≤ M) → ∥u∥ ≤ C*M :=
343345
let ⟨C, hC, h⟩ := v.exists_op_nnnorm_le in ⟨C, hC, λ u, subtype.forall'.mpr h⟩
344346

0 commit comments

Comments
 (0)