Merge branch 'master' of github.com:leanprover-community/mathlib into…

… minkowski

archive/100-theorems-list/9_area_of_a_circle.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 James Arthur, Benjamin Davidson, Andrew Souther. All rights r
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: James Arthur, Benjamin Davidson, Andrew Souther
 -/
-import measure_theory.interval_integral
+import measure_theory.integral.interval_integral
 import analysis.special_functions.sqrt
 
 /-!

archive/imo/imo2001_q6.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2021 Sara Díaz Real. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sara Díaz Real
+-/
+import data.int.basic
+import algebra.associated
+import tactic.linarith
+import tactic.ring
+
+/-!
+# IMO 2001 Q6
+Let $a$, $b$, $c$, $d$ be integers with $a > b > c > d > 0$. Suppose that
+
+$$ a*c + b*d = (a + b - c + d) * (-a + b + c + d). $$
+
+Prove that $a*b + c*d$ is not prime.
+
+-/
+
+variables {a b c d : ℤ}
+
+theorem imo2001_q6 (hd : 0 < d) (hdc : d < c) (hcb : c < b) (hba : b < a)
+  (h : a*c + b*d = (a + b - c + d) * (-a + b + c + d)) :
+  ¬ prime (a*b + c*d) :=
+begin
+  assume h0 : prime (a*b + c*d),
+  have ha : 0 < a, { linarith },
+  have hb : 0 < b, { linarith },
+  have hc : 0 < c, { linarith },
+  -- the key step is to show that `a*c + b*d` divides the product `(a*b + c*d) * (a*d + b*c)`
+  have dvd_mul : a*c + b*d ∣ (a*b + c*d) * (a*d + b*c),
+  { use b^2 + b*d + d^2,
+    have equivalent_sums : a^2 - a*c + c^2 = b^2 + b*d + d^2,
+    { ring_nf at h, nlinarith only [h], },
+    calc  (a * b + c * d) * (a * d + b * c)
+        = a*c * (b^2 + b*d + d^2) + b*d * (a^2 - a*c + c^2) : by ring
+    ... = a*c * (b^2 + b*d + d^2) + b*d * (b^2 + b*d + d^2) : by rw equivalent_sums
+    ... = (a * c + b * d) * (b ^ 2 + b * d + d ^ 2)         : by ring, },
+  -- since `a*b + c*d` is prime (by assumption), it must divide `a*c + b*d` or `a*d + b*c`
+  obtain (h1 : a*b + c*d ∣ a*c + b*d) | (h2 : a*c + b*d ∣ a*d + b*c) :=
+    left_dvd_or_dvd_right_of_dvd_prime_mul h0 dvd_mul,
+  -- in both cases, we derive a contradiction
+  { have aux : 0 < a*c + b*d,         { nlinarith only [ha, hb, hc, hd] },
+    have : a*b + c*d ≤ a*c + b*d,     { from int.le_of_dvd aux h1 },
+    have : ¬ (a*b + c*d ≤ a*c + b*d), { nlinarith only [hba, hcb, hdc, h] },
+    contradiction, },
+  { have aux : 0 < a*d + b*c,         { nlinarith only [ha, hb, hc, hd] },
+    have : a*c + b*d ≤ a*d + b*c,     { from int.le_of_dvd aux h2 },
+    have : ¬ (a*c + b*d ≤ a*d + b*c), { nlinarith only [hba, hdc, h] },
+    contradiction, },
+end

counterexamples/phillips.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.normed_space.hahn_banach
-import measure_theory.lebesgue_measure
+import measure_theory.measure.lebesgue
 
 /-!
 # A counterexample on Pettis integrability

scripts/nolints.txt

@@ -214,9 +214,7 @@ apply_nolint holor_index.drop doc_blame
 apply_nolint holor_index.take doc_blame
 
 -- data/list/defs.lean
-apply_nolint list.permutations_aux doc_blame
 apply_nolint list.permutations_aux.rec doc_blame
-apply_nolint list.permutations_aux2 doc_blame
 apply_nolint list.sublists'_aux doc_blame
 apply_nolint list.sublists_aux doc_blame
 apply_nolint list.sublists_aux₁ doc_blame

src/analysis/calculus/fderiv_measurable.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
 import analysis.calculus.deriv
-import measure_theory.borel_space
+import measure_theory.constructions.borel_space
 
 /-!
 # Derivative is measurable

src/analysis/calculus/fderiv_symmetric.lean

@@ -83,9 +83,10 @@ begin
   { have : filter.tendsto (λ h, h * (∥v∥ + ∥w∥)) (𝓝[Ioi (0:ℝ)] 0) (𝓝 (0 * (∥v∥ + ∥w∥))) :=
       (continuous_id.mul continuous_const).continuous_within_at,
     apply (tendsto_order.1 this).2 δ,
-    simpa using δpos },
+    simpa only [zero_mul] using δpos },
   have E2 : ∀ᶠ h in 𝓝[Ioi (0:ℝ)] 0, (h : ℝ) < 1 :=
-    mem_nhds_within_Ioi_iff_exists_Ioo_subset.2 ⟨(1 : ℝ), by simp, λ x hx, hx.2⟩,
+    mem_nhds_within_Ioi_iff_exists_Ioo_subset.2
+      ⟨(1 : ℝ), by simp only [mem_Ioi, zero_lt_one], λ x hx, hx.2⟩,
   filter_upwards [E1, E2, self_mem_nhds_within],
   -- we consider `h` small enough that all points under consideration belong to this ball,
   -- and also with `0 < h < 1`.
@@ -178,7 +179,7 @@ begin
     ... = ε * ((∥v∥ + ∥w∥) * ∥w∥) * h^2 :
       by { simp only [norm_smul, real.norm_eq_abs, abs_mul, abs_of_nonneg, hpos.le], ring } },
   -- conclude using the mean value inequality
-  have I : ∥g 1 - g 0∥ ≤ ε * ((∥v∥ + ∥w∥) * ∥w∥) * h^2, by simpa using
+  have I : ∥g 1 - g 0∥ ≤ ε * ((∥v∥ + ∥w∥) * ∥w∥) * h^2, by simpa only [mul_one, sub_zero] using
     norm_image_sub_le_of_norm_deriv_le_segment' g_deriv g'_bound 1 (right_mem_Icc.2 zero_le_one),
   convert I using 1,
   { congr' 1,

src/analysis/calculus/parametric_integral.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
-import measure_theory.set_integral
+import measure_theory.integral.set_integral
 import analysis.calculus.mean_value
 
 /-!

src/analysis/convex/integral.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import analysis.convex.basic
-import measure_theory.set_integral
+import measure_theory.integral.set_integral
 
 /-!
 # Jensen's inequality for integrals

src/analysis/fourier.lean

@@ -3,9 +3,9 @@ Copyright (c) 2021 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import measure_theory.continuous_map_dense
-import measure_theory.l2_space
-import measure_theory.haar_measure
+import measure_theory.function.continuous_map_dense
+import measure_theory.function.l2_space
+import measure_theory.measure.haar
 import analysis.complex.circle
 import topology.metric_space.emetric_paracompact
 import topology.continuous_function.stone_weierstrass

src/analysis/normed_space/inner_product.lean

@@ -931,6 +931,9 @@ begin
   exact inner_mul_inner_self_le _ _
 end
 
+lemma norm_inner_le_norm (x y : E) : ∥⟪x, y⟫∥ ≤ ∥x∥ * ∥y∥ :=
+(is_R_or_C.norm_eq_abs _).le.trans (abs_inner_le_norm x y)
+
 /-- Cauchy–Schwarz inequality with norm -/
 lemma abs_real_inner_le_norm (x y : F) : absR ⟪x, y⟫_ℝ ≤ ∥x∥ * ∥y∥ :=
 by { have h := @abs_inner_le_norm ℝ F _ _ x y, simpa using h }
@@ -1373,7 +1376,7 @@ linear_map.mk_continuous
     map_add' := λ x y, inner_add_right,
     map_smul' := λ c x, inner_smul_right }
   ∥v∥
-  (by simpa [is_R_or_C.norm_eq_abs] using abs_inner_le_norm v)
+  (by simpa using norm_inner_le_norm v)
 
 @[simp] lemma inner_right_coe (v : E) : (inner_right v : E → 𝕜) = λ w, ⟪v, w⟫ := rfl
 
@@ -1522,7 +1525,7 @@ lemma is_bounded_bilinear_map_inner : is_bounded_bilinear_map ℝ (λ p : E × E
   smul_right := λ r x y,
     by simp only [← algebra_map_smul 𝕜 r y, algebra_map_eq_of_real, inner_smul_real_right],
   bound := ⟨1, zero_lt_one, λ x y,
-    by { rw [one_mul, is_R_or_C.norm_eq_abs], exact abs_inner_le_norm x y, }⟩ }
+    by { rw [one_mul], exact norm_inner_le_norm x y, }⟩ }
 
 /-- Derivative of the inner product. -/
 def fderiv_inner_clm (p : E × E) : E × E →L[ℝ] 𝕜 := is_bounded_bilinear_map_inner.deriv p

src/analysis/normed_space/normed_group_hom.lean

@@ -5,6 +5,8 @@ Authors: Johan Commelin
 -/
 
 import analysis.normed_space.basic
+import analysis.specific_limits
+import topology.sequences
 
 /-!
 # Normed groups homomorphisms
@@ -127,6 +129,17 @@ theorem antilipschitz_of_norm_ge {K : ℝ≥0} (h : ∀ x, ∥x∥ ≤ K * ∥f
 antilipschitz_with.of_le_mul_dist $
 λ x y, by simpa only [dist_eq_norm, f.map_sub] using h (x - y)
 
+/-- A normed group hom is surjective on the subgroup `K` with constant `C` if every element
+`x` of `K` has a preimage whose norm is bounded above by `C*∥x∥`. This is a more
+abstract version of `f` having a right inverse defined on `K` with operator norm
+at most `C`. -/
+def surjective_on_with (f : normed_group_hom V₁ V₂) (K : add_subgroup V₂) (C : ℝ) : Prop :=
+  ∀ h ∈ K, ∃ g, f g = h ∧ ∥g∥ ≤ C*∥h∥
+
+lemma surjective_on_with.surj_on {f : normed_group_hom V₁ V₂} {K : add_subgroup V₂} {C : ℝ}
+  (h : f.surjective_on_with K C) : set.surj_on f set.univ K :=
+λ x hx, (h x hx).imp $ λ a ⟨ha, _⟩, ⟨set.mem_univ _, ha⟩
+
 /-! ### The operator norm -/
 
 /-- The operator norm of a seminormed group homomorphism is the inf of all its bounds. -/
@@ -186,6 +199,13 @@ lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ∥f x∥ ≤ M * 
   ∥f∥ ≤ M :=
 cInf_le bounds_bdd_below ⟨hMp, hM⟩
 
+lemma op_norm_eq_of_bounds {M : ℝ} (M_nonneg : 0 ≤ M)
+  (h_above : ∀ x, ∥f x∥ ≤ M*∥x∥) (h_below : ∀ N ≥ 0, (∀ x, ∥f x∥ ≤ N*∥x∥) → M ≤ N) :
+  ∥f∥ = M :=
+le_antisymm (f.op_norm_le_bound M_nonneg h_above)
+  ((le_cInf_iff normed_group_hom.bounds_bdd_below ⟨M, M_nonneg, h_above⟩).mpr $
+   λ N ⟨N_nonneg, hN⟩, h_below N N_nonneg hN)
+
 theorem op_norm_le_of_lipschitz {f : normed_group_hom V₁ V₂} {K : ℝ≥0} (hf : lipschitz_with K f) :
   ∥f∥ ≤ K :=
 f.op_norm_le_bound K.2 $ λ x, by simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0
@@ -626,3 +646,110 @@ norm_lift_le _ _ _ hφ
 end equalizer
 
 end normed_group_hom
+
+section controlled_closure
+open filter finset
+open_locale topological_space
+variables {G : Type*} [normed_group G] [complete_space G]
+variables {H : Type*} [normed_group H]
+
+/-- Given `f : normed_group_hom G H` for some complete `G` and a subgroup `K` of `H`, if every
+element `x` of `K` has a preimage under `f` whose norm is at most `C*∥x∥` then the same holds for
+elements of the (topological) closure of `K` with constant `C+ε` instead of `C`, for any
+positive `ε`.
+-/
+lemma controlled_closure_of_complete  {f : normed_group_hom G H} {K : add_subgroup H}
+  {C ε : ℝ} (hC : 0 < C) (hε : 0 < ε) (hyp : f.surjective_on_with K C) :
+  f.surjective_on_with K.topological_closure (C + ε) :=
+begin
+  rintros (h : H) (h_in : h ∈ K.topological_closure),
+  /- We first get rid of the easy case where `h = 0`.-/
+  by_cases hyp_h : h = 0,
+  { rw hyp_h,
+    use 0,
+    simp },
+  /- The desired preimage will be constructed as the sum of a series. Convergence of
+  the series will be guaranteed by completeness of `G`. We first write `h` as the sum
+  of a sequence `v` of elements of `K` which starts close to `h` and then quickly goes to zero.
+  The sequence `b` below quantifies this. -/
+  set b : ℕ → ℝ := λ i, (1/2)^i*(ε*∥h∥/2)/C,
+  have b_pos : ∀ i, 0 < b i,
+  { intro i,
+    field_simp [b, hC],
+    exact div_pos (mul_pos hε (norm_pos_iff.mpr hyp_h))
+                  (mul_pos (by norm_num : (0 : ℝ) < 2^i*2) hC) },
+  obtain ⟨v : ℕ → H, lim_v : tendsto (λ (n : ℕ), ∑ k in range (n + 1), v k) at_top (𝓝 h),
+    v_in : ∀ n, v n ∈ K, hv₀ : ∥v 0 - h∥ < b 0, hv : ∀ n > 0, ∥v n∥ < b n⟩ :=
+    controlled_sum_of_mem_closure h_in b_pos,
+  /- The controlled surjectivity assumption on `f` allows to build preimages `u n` for all
+  elements `v n` of the `v` sequence.-/
+  have : ∀ n, ∃ m' : G, f m' = v n ∧ ∥m'∥ ≤ C * ∥v n∥ := λ (n : ℕ), hyp (v n) (v_in n),
+  choose u hu hnorm_u using this,
+  /- The desired series `s` is then obtained by summing `u`. We then check our choice of
+  `b` ensures `s` is Cauchy. -/
+  set s : ℕ → G := λ n, ∑ k in range (n+1), u k,
+  have : cauchy_seq s,
+  { apply normed_group.cauchy_series_of_le_geometric'' (by norm_num) one_half_lt_one,
+    rintro n (hn : n ≥ 1),
+    calc ∥u n∥ ≤ C*∥v n∥ : hnorm_u n
+    ... ≤ C * b n : mul_le_mul_of_nonneg_left (hv _ $ nat.succ_le_iff.mp hn).le hC.le
+    ... = (1/2)^n * (ε * ∥h∥/2) : by simp [b, mul_div_cancel' _ hC.ne.symm]
+    ... = (ε * ∥h∥/2) * (1/2)^n : mul_comm _ _ },
+  /- We now show that the limit `g` of `s` is the desired preimage. -/
+  obtain ⟨g : G, hg⟩ := cauchy_seq_tendsto_of_complete this,
+  refine ⟨g, _, _⟩,
+  { /- We indeed get a preimage. First note: -/
+    have : f ∘ s = λ n, ∑ k in range (n + 1), v k,
+    { ext n,
+      simp [f.map_sum, hu] },
+    /- In the above equality, the left-hand-side converges to `f g` by continuity of `f` and
+       definition of `g` while the right-hand-side converges to `h` by construction of `v` so
+       `g` is indeed a preimage of `h`. -/
+    rw ← this at lim_v,
+    exact tendsto_nhds_unique ((f.continuous.tendsto g).comp hg) lim_v },
+  { /- Then we need to estimate the norm of `g`, using our careful choice of `b`. -/
+    suffices : ∀ n, ∥s n∥ ≤ (C + ε) * ∥h∥,
+      from le_of_tendsto' (continuous_norm.continuous_at.tendsto.comp hg) this,
+    intros n,
+    have hnorm₀ : ∥u 0∥ ≤ C*b 0 + C*∥h∥,
+    { have := calc
+      ∥v 0∥ ≤ ∥h∥ + ∥v 0 - h∥ : norm_le_insert' _ _
+      ... ≤ ∥h∥ + b 0 : by apply add_le_add_left hv₀.le,
+      calc ∥u 0∥ ≤ C*∥v 0∥ : hnorm_u 0
+      ... ≤ C*(∥h∥ + b 0) : mul_le_mul_of_nonneg_left this hC.le
+      ... = C * b 0 + C * ∥h∥ : by rw [add_comm, mul_add] },
+    have : ∑ k in range (n + 1), C * b k ≤ ε * ∥h∥ := calc
+      ∑ k in range (n + 1), C * b k = (∑ k in range (n + 1), (1 / 2) ^ k) * (ε * ∥h∥ / 2) :
+                     by simp only [b, mul_div_cancel' _ hC.ne.symm, ← sum_mul]
+      ... ≤  2 * (ε * ∥h∥ / 2) : mul_le_mul_of_nonneg_right (sum_geometric_two_le _)
+                                                            (by nlinarith [hε, norm_nonneg h])
+      ... = ε * ∥h∥ : mul_div_cancel' _ two_ne_zero,
+    calc ∥s n∥ ≤ ∑ k in range (n+1), ∥u k∥ : norm_sum_le _ _
+    ... = ∑ k in range n, ∥u (k + 1)∥ + ∥u 0∥ : sum_range_succ' _ _
+    ... ≤ ∑ k in range n, C*∥v (k + 1)∥ + ∥u 0∥ : add_le_add_right (sum_le_sum (λ _ _, hnorm_u _)) _
+    ... ≤ ∑ k in range n, C*b (k+1) + (C*b 0 + C*∥h∥) :
+      add_le_add (sum_le_sum (λ k _, mul_le_mul_of_nonneg_left (hv _ k.succ_pos).le hC.le)) hnorm₀
+    ... = ∑ k in range (n+1), C*b k + C*∥h∥ : by rw [← add_assoc, sum_range_succ']
+    ... ≤ (C+ε)*∥h∥ : by { rw [add_comm, add_mul], apply add_le_add_left this } }
+end
+
+/-- Given `f : normed_group_hom G H` for some complete `G`, if every element `x` of the image of
+an isometric immersion `j : normed_group_hom K H` has a preimage under `f` whose norm is at most
+`C*∥x∥` then the same holds for elements of the (topological) closure of this image with constant
+`C+ε` instead of `C`, for any positive `ε`.
+This is useful in particular if `j` is the inclusion of a normed group into its completion
+(in this case the closure is the full target group).
+-/
+lemma controlled_closure_range_of_complete {f : normed_group_hom G H}
+  {K : Type*} [semi_normed_group K] {j : normed_group_hom K H} (hj : ∀ x, ∥j x∥ = ∥x∥)
+  {C ε : ℝ} (hC : 0 < C) (hε : 0 < ε) (hyp : ∀ k, ∃ g, f g = j k ∧ ∥g∥ ≤ C*∥k∥) :
+  f.surjective_on_with j.range.topological_closure (C + ε) :=
+begin
+  replace hyp : ∀ h ∈ j.range, ∃ g, f g = h ∧ ∥g∥ ≤ C*∥h∥,
+  { intros h h_in,
+    rcases (j.mem_range _).mp h_in with ⟨k, rfl⟩,
+    rw hj,
+    exact hyp k },
+  exact controlled_closure_of_complete hC hε hyp
+end
+end controlled_closure

src/analysis/special_functions/integrals.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson
 -/
-import measure_theory.interval_integral
+import measure_theory.integral.interval_integral
 
 /-!
 # Integration of specific interval integrals

src/data/qpf/multivariate/basic.lean

@@ -68,7 +68,7 @@ matched because they preserve the properties of QPF. The latter example,
 
 each proves that some operations on functors preserves the QPF structure
 
-##reference
+## Reference
 
  * [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
 -/