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

Commit abb3121

Browse files
kim-emkim-em
committed
chore(*): more line lengths (#6472)
 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent f153a85 commit abb3121

67 files changed

Lines changed: 311 additions & 178 deletions

Some content is hidden

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

‎src/analysis/analytic/composition.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -605,7 +605,8 @@ that it is a bijection is not directly possible, but the consequence on sums can
605605
more easily. -/
606606
lemma comp_change_of_variables_sum {α : Type*} [add_comm_monoid α] (m M N : ℕ)
607607
(f : (Σ (n : ℕ), fin n → ℕ) → α) (g : (Σ n, composition n) → α)
608-
(h : ∀ e (he : e ∈ comp_partial_sum_source m M N), f e = g (comp_change_of_variables m M N e he)) :
608+
(h : ∀ e (he : e ∈ comp_partial_sum_source m M N),
609+
f e = g (comp_change_of_variables m M N e he)) :
609610
∑ e in comp_partial_sum_source m M N, f e = ∑ e in comp_partial_sum_target m M N, g e :=
610611
begin
611612
apply finset.sum_bij (comp_change_of_variables m M N),

‎src/analysis/calculus/deriv.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1172,7 +1172,7 @@ end
11721172
end composition
11731173

11741174
section composition_vector
1175-
/-! ### Derivative of the composition of a function between vector spaces and of a function defined on `𝕜` -/
1175+
/-! ### Derivative of the composition of a function between vector spaces and a function on `𝕜` -/
11761176

11771177
variables {l : F → E} {l' : F →L[𝕜] E}
11781178
variable (x)

‎src/analysis/calculus/local_extr.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ This set is used in the proof of Fermat's Theorem (see below), and can be used t
1919
2020
## Main statements
2121
22-
For each theorem name listed below, we also prove similar theorems for `min`, `extr` (if applicable)`,
22+
For each theorem name listed below,
23+
we also prove similar theorems for `min`, `extr` (if applicable)`,
2324
and `(f)deriv` instead of `has_fderiv`.
2425
2526
* `is_local_max_on.has_fderiv_within_at_nonpos` : `f' y ≤ 0` whenever `a` is a local maximum

‎src/analysis/calculus/tangent_cone.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -247,7 +247,8 @@ section unique_diff
247247
/-!
248248
### Properties of `unique_diff_within_at` and `unique_diff_on`
249249
250-
This section is devoted to properties of the predicates `unique_diff_within_at` and `unique_diff_on`. -/
250+
This section is devoted to properties of the predicates
251+
`unique_diff_within_at` and `unique_diff_on`. -/
251252

252253
lemma unique_diff_on.unique_diff_within_at {s : set E} {x} (hs : unique_diff_on 𝕜 s) (h : x ∈ s) :
253254
unique_diff_within_at 𝕜 s x :=

‎src/analysis/calculus/times_cont_diff.lean‎

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -707,7 +707,8 @@ lemma iterated_fderiv_within_zero_eq_comp :
707707

708708
lemma iterated_fderiv_within_succ_apply_left {n : ℕ} (m : fin (n + 1) → E):
709709
(iterated_fderiv_within 𝕜 (n + 1) f s x : (fin (n + 1) → E) → F) m
710-
= (fderiv_within 𝕜 (iterated_fderiv_within 𝕜 n f s) s x : E → (E [×n]→L[𝕜] F)) (m 0) (tail m) := rfl
710+
= (fderiv_within 𝕜 (iterated_fderiv_within 𝕜 n f s) s x : E → (E [×n]→L[𝕜] F))
711+
(m 0) (tail m) := rfl
711712

712713
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
713714
and the derivative of the `n`-th derivative. -/
@@ -864,7 +865,8 @@ begin
864865
have : has_fderiv_within_at (λ (y : E), iterated_fderiv_within 𝕜 m f s y)
865866
(continuous_multilinear_map.curry_left (p x (nat.succ m))) s x :=
866867
(h.fderiv_within m A x hx).congr (λ y hy, (IH (le_of_lt A) hy).symm) (IH (le_of_lt A) hx).symm,
867-
rw [iterated_fderiv_within_succ_eq_comp_left, function.comp_apply, this.fderiv_within (hs x hx)],
868+
rw [iterated_fderiv_within_succ_eq_comp_left, function.comp_apply,
869+
this.fderiv_within (hs x hx)],
868870
exact (continuous_multilinear_map.uncurry_curry_left _).symm }
869871
end
870872

@@ -1420,8 +1422,8 @@ lemma times_cont_diff_of_differentiable_iterated_fderiv {n : with_top ℕ}
14201422
times_cont_diff_iff_continuous_differentiable.2
14211423
⟨λ m hm, (h m hm).continuous, λ m hm, (h m (le_of_lt hm))⟩
14221424

1423-
/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if it is differentiable
1424-
there, and its derivative is `C^n`. -/
1425+
/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if
1426+
it is differentiable there, and its derivative is `C^n`. -/
14251427
theorem times_cont_diff_succ_iff_fderiv {n : ℕ} :
14261428
times_cont_diff 𝕜 ((n + 1) : ℕ) f ↔
14271429
differentiable 𝕜 f ∧ times_cont_diff 𝕜 n (λ y, fderiv 𝕜 f y) :=
@@ -1843,7 +1845,8 @@ lemma times_cont_diff_on.prod {n : with_top ℕ} {s : set E} {f : E → F} {g :
18431845
lemma times_cont_diff_at.prod {n : with_top ℕ} {f : E → F} {g : E → G}
18441846
(hf : times_cont_diff_at 𝕜 n f x) (hg : times_cont_diff_at 𝕜 n g x) :
18451847
times_cont_diff_at 𝕜 n (λx:E, (f x, g x)) x :=
1846-
times_cont_diff_within_at_univ.1 $ times_cont_diff_within_at.prod (times_cont_diff_within_at_univ.2 hf)
1848+
times_cont_diff_within_at_univ.1 $ times_cont_diff_within_at.prod
1849+
(times_cont_diff_within_at_univ.2 hf)
18471850
(times_cont_diff_within_at_univ.2 hg)
18481851

18491852
/--
@@ -2494,7 +2497,8 @@ begin
24942497
have : continuous_linear_map.inverse = O₁ ∘ ring.inverse ∘ O₂ :=
24952498
funext (to_ring_inverse e),
24962499
rw this,
2497-
-- `O₁` and `O₂` are `times_cont_diff`, so we reduce to proving that `ring.inverse` is `times_cont_diff`
2500+
-- `O₁` and `O₂` are `times_cont_diff`,
2501+
-- so we reduce to proving that `ring.inverse` is `times_cont_diff`
24982502
have h₁ : times_cont_diff 𝕜 n O₁,
24992503
from is_bounded_bilinear_map_comp.times_cont_diff.comp
25002504
(times_cont_diff_const.prod times_cont_diff_id),
@@ -2511,9 +2515,10 @@ end map_inverse
25112515
section function_inverse
25122516
open continuous_linear_map
25132517

2514-
/-- If `f` is a local homeomorphism and the point `a` is in its target, and if `f` is `n` times
2515-
continuously differentiable at `f.symm a`, and if the derivative at `f.symm a` is a continuous linear
2516-
equivalence, then `f.symm` is `n` times continuously differentiable at the point `a`.
2518+
/-- If `f` is a local homeomorphism and the point `a` is in its target,
2519+
and if `f` is `n` times continuously differentiable at `f.symm a`,
2520+
and if the derivative at `f.symm a` is a continuous linear equivalence,
2521+
then `f.symm` is `n` times continuously differentiable at the point `a`.
25172522
25182523
This is one of the easy parts of the inverse function theorem: it assumes that we already have
25192524
an inverse function. -/

‎src/analysis/complex/polynomial.lean‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,8 @@ open_locale classical
1818
namespace complex
1919

2020
/- The following proof uses the method given at
21-
<https://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#classical_fta_via_advanced_calculus> -/
21+
<https://ncatlab.org/nlab/show/fundamental+theorem+of+algebra#classical_fta_via_advanced_calculus>
22+
-/
2223
/-- The fundamental theorem of algebra. Every non constant complex polynomial
2324
has a root -/
2425
lemma exists_root {f : polynomial ℂ} (hf : 0 < degree f) : ∃ z : ℂ, is_root f z :=
@@ -47,10 +48,10 @@ let F : polynomial ℂ := C (f.eval z₀) + C (g.eval z₀) * (X - C z₀) ^ n i
4748
let z' := (-f.eval z₀ * (g.eval z₀).abs * δ ^ n /
4849
((f.eval z₀).abs * g.eval z₀)) ^ (n⁻¹ : ℂ) + z₀ in
4950
have hF₁ : F.eval z' = f.eval z₀ - f.eval z₀ * (g.eval z₀).abs * δ ^ n / (f.eval z₀).abs,
50-
by simp only [F, cpow_nat_inv_pow _ hn0, div_eq_mul_inv, eval_pow, mul_assoc, mul_comm (g.eval z₀),
51-
mul_left_comm (g.eval z₀), mul_left_comm (g.eval z₀)⁻¹, mul_inv', inv_mul_cancel hg0,
52-
eval_C, eval_add, eval_neg, sub_eq_add_neg, eval_mul, eval_X, add_neg_cancel_right,
53-
neg_mul_eq_neg_mul_symm, mul_one, div_eq_mul_inv];
51+
by simp only [F, cpow_nat_inv_pow _ hn0, div_eq_mul_inv, eval_pow, mul_assoc,
52+
mul_comm (g.eval z₀), mul_left_comm (g.eval z₀), mul_left_comm (g.eval z₀)⁻¹, mul_inv',
53+
inv_mul_cancel hg0, eval_C, eval_add, eval_neg, sub_eq_add_neg, eval_mul, eval_X,
54+
add_neg_cancel_right, neg_mul_eq_neg_mul_symm, mul_one, div_eq_mul_inv];
5455
simp only [mul_comm, mul_left_comm, mul_assoc],
5556
have hδs : (g.eval z₀).abs * δ ^ n / (f.eval z₀).abs < 1,
5657
from (div_lt_one hf0').2 $ (lt_div_iff' hg0').1 $

‎src/analysis/convex/extrema.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,8 @@ end
9393
lemma is_max_on.of_is_local_max_on_of_concave_on {f : E → β} {a : E}
9494
(a_in_s : a ∈ s) (h_localmax: is_local_max_on f s a) (h_conc : concave_on s f) :
9595
∀ x ∈ s, f x ≤ f a :=
96-
@is_min_on.of_is_local_min_on_of_convex_on _ (order_dual β) _ _ _ _ _ _ _ _ s f a a_in_s h_localmax h_conc
96+
@is_min_on.of_is_local_min_on_of_convex_on
97+
_ (order_dual β) _ _ _ _ _ _ _ _ s f a a_in_s h_localmax h_conc
9798

9899
/-- A local minimum of a convex function is a global minimum. -/
99100
lemma is_min_on.of_is_local_min_of_convex_univ {f : E → β} {a : E}

‎src/analysis/normed_space/bounded_linear_maps.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,8 @@ end is_bounded_linear_map
145145
section
146146
variables {ι : Type*} [decidable_eq ι] [fintype ι]
147147

148-
/-- Taking the cartesian product of two continuous multilinear maps is a bounded linear operation. -/
148+
/-- Taking the cartesian product of two continuous multilinear maps
149+
is a bounded linear operation. -/
149150
lemma is_bounded_linear_map_prod_multilinear
150151
{E : ι → Type*} [∀i, normed_group (E i)] [∀i, normed_space 𝕜 (E i)] :
151152
is_bounded_linear_map 𝕜
@@ -251,7 +252,8 @@ lemma is_bounded_bilinear_map.is_bounded_linear_map_left (h : is_bounded_bilinea
251252
... = C * (∥y∥ + 1) * ∥x∥ : by ring
252253
end }
253254

254-
lemma is_bounded_bilinear_map.is_bounded_linear_map_right (h : is_bounded_bilinear_map 𝕜 f) (x : E) :
255+
lemma is_bounded_bilinear_map.is_bounded_linear_map_right
256+
(h : is_bounded_bilinear_map 𝕜 f) (x : E) :
255257
is_bounded_linear_map 𝕜 (λ y, f (x, y)) :=
256258
{ map_add := λ y y', h.add_right _ _ _,
257259
map_smul := λ c y, h.smul_right _ _ _,
@@ -374,7 +376,8 @@ def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map 𝕜 f) (p : E ×
374376
≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : norm_add_le_of_le (hC _ _) (hC _ _)
375377
... ≤ C * ∥p.1∥ * ∥q∥ + C * ∥q∥ * ∥p.2∥ : begin
376378
apply add_le_add,
377-
exact mul_le_mul_of_nonneg_left (le_max_right _ _) (mul_nonneg (le_of_lt Cpos) (norm_nonneg _)),
379+
exact mul_le_mul_of_nonneg_left
380+
(le_max_right _ _) (mul_nonneg (le_of_lt Cpos) (norm_nonneg _)),
378381
apply mul_le_mul_of_nonneg_right _ (norm_nonneg _),
379382
exact mul_le_mul_of_nonneg_left (le_max_left _ _) (le_of_lt Cpos),
380383
end
@@ -418,7 +421,8 @@ end bilinear_map
418421
lemma linear_map.norm_apply_of_isometry (f : E →ₗ[𝕜] F) {x : E} (hf : isometry f) : ∥f x∥ = ∥x∥ :=
419422
by { simp_rw [←dist_zero_right, ←f.map_zero], exact isometry.dist_eq hf _ _ }
420423

421-
/-- Construct a continuous linear equiv from a linear map that is also an isometry with full range. -/
424+
/-- Construct a continuous linear equiv from
425+
a linear map that is also an isometry with full range. -/
422426
def continuous_linear_equiv.of_isometry (f : E →ₗ[𝕜] F) (hf : isometry f) (hfr : f.range = ⊤) :
423427
E ≃L[𝕜] F :=
424428
continuous_linear_equiv.of_homothety

‎src/analysis/normed_space/multilinear.lean‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -732,7 +732,8 @@ protected def pi_field_equiv : G ≃L[𝕜] (continuous_multilinear_map 𝕜 (λ
732732
exact multilinear_map.mk_continuous_norm_le _ (norm_nonneg _) _
733733
end,
734734
continuous_inv_fun := begin
735-
refine (continuous_multilinear_map.pi_field_equiv_aux 𝕜 ι G).symm.to_linear_map.continuous_of_bound
735+
refine
736+
(continuous_multilinear_map.pi_field_equiv_aux 𝕜 ι G).symm.to_linear_map.continuous_of_bound
736737
(1 : ℝ) (λf, _),
737738
rw one_mul,
738739
change ∥f (λi, 1)∥ ≤ ∥f∥,
@@ -1012,14 +1013,16 @@ by { ext m, simp }
10121013

10131014
variables (𝕜 Ei G)
10141015

1015-
/-- The space of continuous multilinear maps on `Π(i : fin (n+1)), Ei i` is canonically isomorphic to
1016+
/--
1017+
The space of continuous multilinear maps on `Π(i : fin (n+1)), Ei i` is canonically isomorphic to
10161018
the space of continuous multilinear maps on `Π(i : fin n), Ei i.cast_succ` with values in the space
10171019
of continuous linear maps on `Ei (last n)`, by separating the last variable. We register this
10181020
isomorphism as a continuous linear equiv in `continuous_multilinear_curry_right_equiv 𝕜 Ei G`.
10191021
The algebraic version (without topology) is given in `multilinear_curry_right_equiv 𝕜 Ei G`.
10201022
10211023
The direct and inverse maps are given by `f.uncurry_right` and `f.curry_right`. Use these
1022-
unless you need the full framework of linear isometric equivs. -/
1024+
unless you need the full framework of linear isometric equivs.
1025+
-/
10231026
def continuous_multilinear_curry_right_equiv :
10241027
(continuous_multilinear_map 𝕜 (λ(i : fin n), Ei i.cast_succ) (Ei (last n) →L[𝕜] G)) ≃ₗᵢ[𝕜]
10251028
(continuous_multilinear_map 𝕜 Ei G) :=

‎src/analysis/normed_space/operator_norm.lean‎

Lines changed: 16 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -31,10 +31,11 @@ lemma exists_pos_bound_of_bound {f : E → F} (M : ℝ) (h : ∀x, ∥f x∥ ≤
3131
... ≤ max M 1 * ∥x∥ : mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) ⟩
3232

3333
section normed_field
34-
/- Most statements in this file require the field to be non-discrete, as this is necessary
35-
to deduce an inequality `∥f x∥ ≤ C ∥x∥` from the continuity of f. However, the other direction always
36-
holds. In this section, we just assume that `𝕜` is a normed field. In the remainder of the file,
37-
it will be non-discrete. -/
34+
/-! Most statements in this file require the field to be non-discrete,
35+
as this is necessary to deduce an inequality `∥f x∥ ≤ C ∥x∥` from the continuity of f.
36+
However, the other direction always holds.
37+
In this section, we just assume that `𝕜` is a normed field.
38+
In the remainder of the file, it will be non-discrete. -/
3839

3940
variables [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →ₗ[𝕜] F)
4041

@@ -89,7 +90,8 @@ let φ : E →ₗ[𝕜] F := ⟨f, h_add, h_smul⟩ in φ.continuous_of_bound C
8990
@[simp] lemma linear_map.mk_continuous_apply (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
9091
f.mk_continuous C h x = f x := rfl
9192

92-
@[simp, norm_cast] lemma linear_map.mk_continuous_of_exists_bound_coe (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) :
93+
@[simp, norm_cast] lemma linear_map.mk_continuous_of_exists_bound_coe
94+
(h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) :
9395
((f.mk_continuous_of_exists_bound h) : E →ₗ[𝕜] F) = f := rfl
9496

9597
@[simp] lemma linear_map.mk_continuous_of_exists_bound_apply (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
@@ -219,7 +221,8 @@ f.mk_continuous a (λ x, le_of_eq (hf x))
219221

220222
variable (𝕜)
221223

222-
lemma to_span_singleton_homothety (x : E) (c : 𝕜) : ∥linear_map.to_span_singleton 𝕜 E x c∥ = ∥x∥ * ∥c∥ :=
224+
lemma to_span_singleton_homothety (x : E) (c : 𝕜) :
225+
∥linear_map.to_span_singleton 𝕜 E x c∥ = ∥x∥ * ∥c∥ :=
223226
by {rw mul_comm, exact norm_smul _ _}
224227

225228
/-- Given an element `x` of a normed space `E` over a field `𝕜`, the natural continuous
@@ -1146,10 +1149,14 @@ variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
11461149

11471150
variables {𝕜}
11481151

1149-
variables {E' F' : Type*} [normed_group E'] [normed_group F'] [normed_space 𝕜 E'] [normed_space 𝕜 F']
1152+
variables {E' F' : Type*} [normed_group E'] [normed_group F']
1153+
[normed_space 𝕜 E'] [normed_space 𝕜 F']
11501154

1151-
/-- Compose a bilinear map `E →L[𝕜] F →L[𝕜] G` with two linear maps `E' →L[𝕜] E` and `F' →L[𝕜] F`. -/
1152-
def bilinear_comp (f : E →L[𝕜] F →L[𝕜] G) (gE : E' →L[𝕜] E) (gF : F' →L[𝕜] F) : E' →L[𝕜] F' →L[𝕜] G :=
1155+
/--
1156+
Compose a bilinear map `E →L[𝕜] F →L[𝕜] G` with two linear maps `E' →L[𝕜] E` and `F' →L[𝕜] F`.
1157+
-/
1158+
def bilinear_comp (f : E →L[𝕜] F →L[𝕜] G) (gE : E' →L[𝕜] E) (gF : F' →L[𝕜] F) :
1159+
E' →L[𝕜] F' →L[𝕜] G :=
11531160
((f.comp gE).flip.comp gF).flip
11541161

11551162
@[simp] lemma bilinear_comp_apply (f : E →L[𝕜] F →L[𝕜] G) (gE : E' →L[𝕜] E) (gF : F' →L[𝕜] F)

0 commit comments

Comments
 (0)