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

Commit ce11c3c

Browse files
eric-wiesereric-wieser
committed
refactor(linear_algebra/{multilinear,pi_tensor_product}): remove the decidable_eq argument (#10140)
There is no need to include this argument in the type of `multilinear_map`, as it is only used to state the propositions. Instead, we move it into a binder in the `map_add` and `map_smul` fields. The same trick is done for the relation for `pi_tensor_product`. The benefit here is pretty marginal; the main one is that `mutlilinear_map.mk_pi_algebra` no longer requires a `decidable_eq I` instance. However, it still requires `fintype I`, and in practice all computably finite types are also computably decidable. This does at least mean that `0 : multilinear_map ...` rightfully no longer requires decidable equality! The downside of this PR is that the `map_add'` and `map_smul'` fields are often more annoying to prove as there are sometimes duplicate decidable instances to eliminate. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/A.20possible.20diamond/near/260179946)
1 parent 6e272cd commit ce11c3c

15 files changed

Lines changed: 281 additions & 198 deletions

File tree

‎src/analysis/analytic/composition.lean‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -181,10 +181,12 @@ def comp_along_composition {n : ℕ}
181181
(f : continuous_multilinear_map 𝕜 (λ (i : fin c.length), F) G) :
182182
continuous_multilinear_map 𝕜 (λ i : fin n, E) G :=
183183
{ to_fun := λ v, f (p.apply_composition c v),
184-
map_add' := λ v i x y, by simp only [apply_composition_update,
185-
continuous_multilinear_map.map_add],
186-
map_smul' := λ v i c x, by simp only [apply_composition_update,
187-
continuous_multilinear_map.map_smul],
184+
map_add' := λ _ v i x y, by
185+
{ cases subsingleton.elim ‹_› (fin.decidable_eq _),
186+
simp only [apply_composition_update, continuous_multilinear_map.map_add] },
187+
map_smul' := λ _ v i c x, by
188+
{ cases subsingleton.elim ‹_› (fin.decidable_eq _),
189+
simp only [apply_composition_update, continuous_multilinear_map.map_smul] },
188190
cont := f.cont.comp $ continuous_pi $ λ i, (coe_continuous _).comp $ continuous_pi $ λ j,
189191
continuous_apply _, }
190192

‎src/analysis/analytic/inverse.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -393,7 +393,7 @@ begin
393393
(λ (k : ℕ), (fintype.pi_finset (λ (i : fin k), Ico 1 n) : finset (fin k → ℕ)))
394394
(λ n e, ∏ (j : fin n), r * (a ^ e j * p (e j)))],
395395
apply sum_congr rfl (λ j hj, _),
396-
simp only [← @multilinear_map.mk_pi_algebra_apply ℝ (fin j) _ _ ℝ],
396+
simp only [← @multilinear_map.mk_pi_algebra_apply ℝ (fin j) _ ℝ],
397397
simp only [← multilinear_map.map_sum_finset (multilinear_map.mk_pi_algebra ℝ (fin j) ℝ)
398398
(λ k (m : ℕ), r * (a ^ m * p m))],
399399
simp only [multilinear_map.mk_pi_algebra_apply],

‎src/analysis/normed_space/bounded_linear_maps.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ artifact, really.
4949
-/
5050

5151
noncomputable theory
52-
open_locale classical big_operators topology
52+
open_locale big_operators topology
5353

5454
open filter (tendsto) metric continuous_linear_map
5555

@@ -183,7 +183,7 @@ end
183183
end is_bounded_linear_map
184184

185185
section
186-
variables {ι : Type*} [decidable_eq ι] [fintype ι]
186+
variables {ι : Type*} [fintype ι]
187187

188188
/-- Taking the cartesian product of two continuous multilinear maps
189189
is a bounded linear operation. -/
@@ -441,7 +441,7 @@ lemma is_bounded_bilinear_map_smul_right :
441441
/-- The composition of a continuous linear map with a continuous multilinear map is a bounded
442442
bilinear operation. -/
443443
lemma is_bounded_bilinear_map_comp_multilinear {ι : Type*} {E : ι → Type*}
444-
[decidable_eq ι] [fintype ι] [∀ i, normed_add_comm_group (E i)] [∀ i, normed_space 𝕜 (E i)] :
444+
[fintype ι] [∀ i, normed_add_comm_group (E i)] [∀ i, normed_space 𝕜 (E i)] :
445445
is_bounded_bilinear_map 𝕜 (λ p : (F →L[𝕜] G) × (continuous_multilinear_map 𝕜 E F),
446446
p.1.comp_continuous_multilinear_map p.2) :=
447447
(comp_continuous_multilinear_mapL 𝕜 E F G).is_bounded_bilinear_map

‎src/analysis/normed_space/multilinear.lean‎

Lines changed: 22 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ approach, it turns out that direct proofs are easier and more efficient.
5454
-/
5555

5656
noncomputable theory
57-
open_locale classical big_operators nnreal
57+
open_locale big_operators nnreal
5858
open finset metric
5959

6060
local attribute [instance, priority 1001]
@@ -77,7 +77,7 @@ universes u v v' wE wE₁ wE' wEi wG wG'
7777
variables {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {n : ℕ}
7878
{E : ι → Type wE} {E₁ : ι → Type wE₁} {E' : ι' → Type wE'} {Ei : fin n.succ → Type wEi}
7979
{G : Type wG} {G' : Type wG'}
80-
[decidable_eq ι] [fintype ι] [decidable_eq ι'] [fintype ι'] [nontrivially_normed_field 𝕜]
80+
[fintype ι] [fintype ι'] [nontrivially_normed_field 𝕜]
8181
[Π i, normed_add_comm_group (E i)] [Π i, normed_space 𝕜 (E i)]
8282
[Π i, normed_add_comm_group (E₁ i)] [Π i, normed_space 𝕜 (E₁ i)]
8383
[Π i, normed_add_comm_group (E' i)] [Π i, normed_space 𝕜 (E' i)]
@@ -137,7 +137,7 @@ using the multilinearity. Here, we give a precise but hard to use version. See
137137
`‖f m - f m'‖ ≤
138138
C * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...`,
139139
where the other terms in the sum are the same products where `1` is replaced by any `i`. -/
140-
lemma norm_image_sub_le_of_bound' {C : ℝ} (hC : 0 ≤ C)
140+
lemma norm_image_sub_le_of_bound' [decidable_eq ι] {C : ℝ} (hC : 0 ≤ C)
141141
(H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : Πi, E i) :
142142
‖f m₁ - f m₂‖ ≤
143143
C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
@@ -182,6 +182,7 @@ lemma norm_image_sub_le_of_bound {C : ℝ} (hC : 0 ≤ C)
182182
(H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : Πi, E i) :
183183
‖f m₁ - f m₂‖ ≤ C * (fintype.card ι) * (max ‖m₁‖ ‖m₂‖) ^ (fintype.card ι - 1) * ‖m₁ - m₂‖ :=
184184
begin
185+
letI := classical.dec_eq ι,
185186
have A : ∀ (i : ι), ∏ j, (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖)
186187
≤ ‖m₁ - m₂‖ * (max ‖m₁‖ ‖m₂‖) ^ (fintype.card ι - 1),
187188
{ assume i,
@@ -541,7 +542,7 @@ For a less precise but more usable version, see `norm_image_sub_le`. The bound r
541542
`‖f m - f m'‖ ≤
542543
‖f‖ * ‖m 1 - m' 1‖ * max ‖m 2‖ ‖m' 2‖ * max ‖m 3‖ ‖m' 3‖ * ... * max ‖m n‖ ‖m' n‖ + ...`,
543544
where the other terms in the sum are the same products where `1` is replaced by any `i`.-/
544-
lemma norm_image_sub_le' (m₁ m₂ : Πi, E i) :
545+
lemma norm_image_sub_le' [decidable_eq ι] (m₁ m₂ : Πi, E i) :
545546
‖f m₁ - f m₂‖ ≤
546547
‖f‖ * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
547548
f.to_multilinear_map.norm_image_sub_le_of_bound' (norm_nonneg _) f.le_op_norm _ _
@@ -633,13 +634,15 @@ begin
633634
-- Next, we show that this `F` is multilinear,
634635
let Fmult : multilinear_map 𝕜 E G :=
635636
{ to_fun := F,
636-
map_add' := λ v i x y, begin
637+
map_add' := λ _ v i x y, begin
638+
resetI,
637639
have A := hF (function.update v i (x + y)),
638640
have B := (hF (function.update v i x)).add (hF (function.update v i y)),
639641
simp at A B,
640642
exact tendsto_nhds_unique A B
641643
end,
642-
map_smul' := λ v i c x, begin
644+
map_smul' := λ _ v i c x, begin
645+
resetI,
643646
have A := hF (function.update v i (c • x)),
644647
have B := filter.tendsto.smul (@tendsto_const_nhds _ ℕ _ c _) (hF (function.update v i x)),
645648
simp at A B,
@@ -722,7 +725,7 @@ variables {𝕜 ι} {A : Type*} [normed_comm_ring A] [normed_algebra 𝕜 A]
722725
lemma norm_mk_pi_algebra_le [nonempty ι] :
723726
‖continuous_multilinear_map.mk_pi_algebra 𝕜 ι A‖ ≤ 1 :=
724727
begin
725-
have := λ f, @op_norm_le_bound 𝕜 ι (λ i, A) A _ _ _ _ _ _ _ f _ zero_le_one,
728+
have := λ f, @op_norm_le_bound 𝕜 ι (λ i, A) A _ _ _ _ _ _ f _ zero_le_one,
726729
refine this _ _,
727730
intros m,
728731
simp only [continuous_multilinear_map.mk_pi_algebra_apply, one_mul],
@@ -733,7 +736,7 @@ lemma norm_mk_pi_algebra_of_empty [is_empty ι] :
733736
‖continuous_multilinear_map.mk_pi_algebra 𝕜 ι A‖ = ‖(1 : A)‖ :=
734737
begin
735738
apply le_antisymm,
736-
{ have := λ f, @op_norm_le_bound 𝕜 ι (λ i, A) A _ _ _ _ _ _ _ f _ (norm_nonneg (1 : A)),
739+
{ have := λ f, @op_norm_le_bound 𝕜 ι (λ i, A) A _ _ _ _ _ _ f _ (norm_nonneg (1 : A)),
737740
refine this _ _,
738741
simp, },
739742
{ convert ratio_le_op_norm _ (λ _, (1 : A)),
@@ -759,7 +762,7 @@ variables {𝕜 n} {A : Type*} [normed_ring A] [normed_algebra 𝕜 A]
759762
lemma norm_mk_pi_algebra_fin_succ_le :
760763
‖continuous_multilinear_map.mk_pi_algebra_fin 𝕜 n.succ A‖ ≤ 1 :=
761764
begin
762-
have := λ f, @op_norm_le_bound 𝕜 (fin n.succ) (λ i, A) A _ _ _ _ _ _ _ f _ zero_le_one,
765+
have := λ f, @op_norm_le_bound 𝕜 (fin n.succ) (λ i, A) A _ _ _ _ _ _ f _ zero_le_one,
763766
refine this _ _,
764767
intros m,
765768
simp only [continuous_multilinear_map.mk_pi_algebra_fin_apply, one_mul, list.of_fn_eq_map,
@@ -781,7 +784,7 @@ lemma norm_mk_pi_algebra_fin_zero :
781784
‖continuous_multilinear_map.mk_pi_algebra_fin 𝕜 0 A‖ = ‖(1 : A)‖ :=
782785
begin
783786
refine le_antisymm _ _,
784-
{ have := λ f, @op_norm_le_bound 𝕜 (fin 0) (λ i, A) A _ _ _ _ _ _ _ f _ (norm_nonneg (1 : A)),
787+
{ have := λ f, @op_norm_le_bound 𝕜 (fin 0) (λ i, A) A _ _ _ _ _ _ f _ (norm_nonneg (1 : A)),
785788
refine this _ _,
786789
simp, },
787790
{ convert ratio_le_op_norm _ (λ _, (1 : A)),
@@ -926,10 +929,10 @@ multilinear_map.mk_continuous
926929
ring_hom.id_apply] }
927930
(‖f‖ * ∏ i, ‖m i‖) $ λ x,
928931
by { rw mul_right_comm, exact (f x).le_of_op_norm_le _ (f.le_op_norm x) },
929-
map_add' := λ m i x y,
932+
map_add' := λ _ m i x y,
930933
by { ext1, simp only [add_apply, continuous_multilinear_map.map_add, linear_map.coe_mk,
931934
linear_map.mk_continuous_apply]},
932-
map_smul' := λ m i c x,
935+
map_smul' := λ _ m i c x,
933936
by { ext1, simp only [coe_smul', continuous_multilinear_map.map_smul, linear_map.coe_mk,
934937
linear_map.mk_continuous_apply, pi.smul_apply]} }
935938
‖f‖ $ λ m,
@@ -988,8 +991,8 @@ def mk_continuous_multilinear (f : multilinear_map 𝕜 E (multilinear_map 𝕜
988991
continuous_multilinear_map 𝕜 E (continuous_multilinear_map 𝕜 E' G) :=
989992
mk_continuous
990993
{ to_fun := λ m, mk_continuous (f m) (C * ∏ i, ‖m i‖) $ H m,
991-
map_add' := λ m i x y, by { ext1, simp },
992-
map_smul' := λ m i c x, by { ext1, simp } }
994+
map_add' := λ _ m i x y, by { ext1, simp },
995+
map_smul' := λ _ m i c x, by { ext1, simp } }
993996
(max C 0) $ λ m, ((f m).mk_continuous_norm_le' _).trans_eq $
994997
by { rw [max_mul_of_nonneg, zero_mul], exact prod_nonneg (λ _ _, norm_nonneg _) }
995998

@@ -1069,7 +1072,7 @@ linear_map.mk_continuous
10691072
rfl
10701073

10711074
lemma norm_comp_continuous_linear_mapL_le (f : Π i, E i →L[𝕜] E₁ i) :
1072-
‖@comp_continuous_linear_mapL 𝕜 ι E E₁ G _ _ _ _ _ _ _ _ _ f‖ ≤ (∏ i, ‖f i‖) :=
1075+
‖@comp_continuous_linear_mapL 𝕜 ι E E₁ G _ _ _ _ _ _ _ _ f‖ ≤ (∏ i, ‖f i‖) :=
10731076
linear_map.mk_continuous_norm_le _ (prod_nonneg $ λ i _, norm_nonneg _) _
10741077

10751078
variable (G)
@@ -1276,8 +1279,8 @@ def continuous_multilinear_map.uncurry_right
12761279
continuous_multilinear_map 𝕜 Ei G :=
12771280
let f' : multilinear_map 𝕜 (λ(i : fin n), Ei i.cast_succ) (Ei (last n) →ₗ[𝕜] G) :=
12781281
{ to_fun := λ m, (f m).to_linear_map,
1279-
map_add' := λ m i x y, by simp,
1280-
map_smul' := λ m i c x, by simp } in
1282+
map_add' := λ _ m i x y, by simp,
1283+
map_smul' := λ _ m i c x, by simp } in
12811284
(@multilinear_map.uncurry_right 𝕜 n Ei G _ _ _ _ _ f').mk_continuous
12821285
(‖f‖) (λm, f.norm_map_init_le m)
12831286

@@ -1295,8 +1298,8 @@ def continuous_multilinear_map.curry_right
12951298
let f' : multilinear_map 𝕜 (λ(i : fin n), Ei i.cast_succ) (Ei (last n) →L[𝕜] G) :=
12961299
{ to_fun := λm, (f.to_multilinear_map.curry_right m).mk_continuous
12971300
(‖f‖ * ∏ i, ‖m i‖) $ λx, f.norm_map_snoc_le m x,
1298-
map_add' := λ m i x y, by { simp, refl },
1299-
map_smul' := λ m i c x, by { simp, refl } } in
1301+
map_add' := λ _ m i x y, by { simp, refl },
1302+
map_smul' := λ _ m i c x, by { simp, refl } } in
13001303
f'.mk_continuous (‖f‖) (λm, linear_map.mk_continuous_norm_le _
13011304
(mul_nonneg (norm_nonneg _) (prod_nonneg (λj hj, norm_nonneg _))) _)
13021305

@@ -1518,8 +1521,6 @@ variables {𝕜 G G'}
15181521

15191522
section
15201523

1521-
variable [decidable_eq (ι ⊕ ι')]
1522-
15231524
/-- A continuous multilinear map with variables indexed by `ι ⊕ ι'` defines a continuous multilinear
15241525
map with variables indexed by `ι` taking values in the space of continuous multilinear maps with
15251526
variables indexed by `ι'`. -/

0 commit comments

Comments
 (0)