feat(analysis/cauchy_equation): Add Cauchy's Functional Equation

src/analysis/cauchy_equation.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2022 Mantas Bakšys. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mantas Bakšys
+-/
+import measure_theory.measure.lebesgue.eq_haar
+
+/-!
+# Cauchy's Functional Equation
+
+This file contains the classical results about the Cauchy's functional equation
+`f (x + y) = f x + f y` for functions `f : ℝ → ℝ`. In this file, we prove that the solutions to this
+equation are linear up to the case when `f` is a Lebesgue measurable functions, while also deducing
+intermediate well-known variants.
+-/
+
+open add_monoid_hom measure_theory measure_theory.measure metric nnreal set
+open_locale pointwise topology
+
+section seminormed_group
+open topological_space
+variables {G H : Type*} [seminormed_add_group G] [topological_add_group G] [is_R_or_C H] {s : set G}
+
+lemma add_monoid_hom.continuous_of_bounded_nhds_zero (f : G →+ H) (hs : s ∈ 𝓝 (0 : G))
+  (hbounded : bounded (f '' s)) : continuous f :=
+begin
+  obtain ⟨δ, hδ, hUε⟩ := metric.mem_nhds_iff.mp hs,
+  obtain ⟨C, hC⟩ := (bounded_iff_subset_ball 0).1 (hbounded.mono $ image_subset f hUε),
+  refine continuous_of_continuous_at_zero _ (continuous_at_iff.2 $ λ ε (hε : _ < _), _),
+  simp only [gt_iff_lt, dist_zero_right, _root_.map_zero, exists_prop],
+  obtain ⟨n, hn⟩ := exists_nat_gt (C / ε),
+  obtain hC₀ | hC₀ := le_or_lt C 0,
+  { refine ⟨δ, hδ, λ x hxδ, _⟩,
+    rwa [eq_of_dist_eq_zero (dist_nonneg.antisymm' $ (mem_closed_ball.1 $ hC $ mem_image_of_mem f $
+      mem_ball_zero_iff.2 hxδ).trans hC₀), norm_zero] },
+  have hnpos : 0 < (n : ℝ) := (div_pos hC₀ hε).trans hn,
+  refine ⟨δ / n, div_pos hδ hnpos, λ x hxδ, _⟩,
+  have h2 : f (n • x) = n • f x := map_nsmul f _ _,
+  have hn' : (n : H) ≠ 0 := nat.cast_ne_zero.2 (by { rintro rfl, simpa using hnpos }),
+  simp_rw [nsmul_eq_mul, mul_comm (n : H), ←div_eq_iff hn'] at h2,
+  replace hxδ : ‖n • x‖ < δ,
+  { refine (norm_nsmul_le _ _).trans_lt _,
+    simpa only [norm_mul, real.norm_coe_nat, lt_div_iff hnpos, mul_comm] using hxδ },
+  rw [←h2, norm_div, is_R_or_C.norm_nat_cast, div_lt_iff' hnpos, ←mem_ball_zero_iff],
+  rw div_lt_iff hε at hn,
+  exact hC.trans (closed_ball_subset_ball hn) (mem_image_of_mem _ $ mem_ball_zero_iff.2 hxδ),
+end
+
+end seminormed_group
+
+variables {ι : Type*} [fintype ι] {s : set ℝ} {a : ℝ}
+
+local notation `ℝⁿ` := ι → ℝ
+
+lemma add_monoid_hom.measurable_of_continuous (f : ℝ →+ ℝ) (h : measurable f) : continuous f :=
+let ⟨s, hs, hbdd⟩ := h.exists_nhds_zero_bounded f in f.continuous_of_bounded_nhds_zero hs hbdd
+
+-- do we want this one and where would it go?
+lemma is_linear_map_iff_apply_eq_apply_one_mul {M : Type*} [comm_semiring M] (f : M →+ M) :
+  is_linear_map M f ↔ ∀ x : M, f x = f 1 * x :=
+begin
+  refine ⟨λ h x, _, λ h, ⟨map_add f, λ c x, _⟩⟩,
+  { convert h.2 x 1 using 1,
+    { simp only [algebra.id.smul_eq_mul, mul_one] },
+    { simp only [mul_comm, algebra.id.smul_eq_mul] }},
+  { rw [smul_eq_mul, smul_eq_mul, h (c * x), h x, ←mul_assoc, mul_comm _ c, mul_assoc] }
+end
+
+lemma is_linear_rat (f : ℝ →+ ℝ) (q : ℚ) : f q = f 1 * q :=
+begin
+  have := map_rat_cast_smul f ℚ ℚ q (1 : ℝ),
+  simpa [mul_comm] using this,
+end
+
+lemma additive_is_bounded_of_bounded_on_interval (f : ℝ →+ ℝ) (hs : s ∈ 𝓝 a)
+  (h : bounded (f '' s)) : ∃ V, V ∈ 𝓝 (0 : ℝ) ∧ bounded (f '' V) :=
+begin
+  rcases metric.mem_nhds_iff.mp hs with ⟨δ, hδ, hδa⟩,
+  refine ⟨ball 0 δ, ball_mem_nhds 0 hδ, _⟩,
+  rw bounded_iff_forall_norm_le,
+  simp only [mem_image, mem_ball_zero_iff, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂],
+  obtain ⟨M, hM⟩ := bounded_iff_forall_norm_le.1 h,
+  simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hM,
+  refine ⟨M + M, λ x hxδ, (norm_le_add_norm_add _ $ f a).trans $ add_le_add _ $ hM _ $ hδa _⟩,
+  { rw ←map_add f,
+    refine hM _ (hδa _),
+    simp only [mem_ball],
+    convert hxδ,
+    rw [←dist_zero_right, ←dist_add_right x 0 a, zero_add] },
+  { simpa [mem_ball, dist_self] }
+end
+
+-- to generalize
+lemma add_monoid_hom.continuous_at_iff_continuous_at_zero (f : ℝ →+ ℝ) :
+  continuous_at f a ↔ continuous_at f 0 :=
+begin
+  refine ⟨λ ha, continuous_at_iff.2 $ λ ε hε, Exists₂.imp (λ δ hδ, _) (continuous_at_iff.1 ha ε hε),
+    λ h, (continuous_of_continuous_at_zero f h).continuous_at⟩,
+  refine λ hδf y hyδ, _,
+  replace hyδ : dist (y + a) a < δ,
+  { convert hyδ using 1,
+    simp only [dist_eq_norm, sub_zero, add_sub_cancel] },
+  convert hδf hyδ using 1,
+  simp only [dist_eq_norm, map_sub, _root_.map_add, _root_.map_zero, sub_zero, add_sub_cancel],
+end
+
+lemma continuous.is_linear_real (f : ℝ →+ ℝ) (h : continuous f) : is_linear_map ℝ f :=
+(f.to_real_linear_map h).to_linear_map.is_linear
+
+lemma is_linear_map_real_of_bounded_nhds (f : ℝ →+ ℝ) (hs : s ∈ 𝓝 a) (hf : bounded (f '' s)) :
+  is_linear_map ℝ f :=
+let ⟨V, hV0, hVb⟩ := additive_is_bounded_of_bounded_on_interval f hs hf in
+  (f.continuous_of_bounded_nhds_zero hV0 hVb).is_linear_real f
+
+lemma monotone_on.is_linear_map_real (f : ℝ →+ ℝ) (hs : s ∈ 𝓝 a) (hf : monotone_on f s) :
+  is_linear_map ℝ f :=
+begin
+  obtain ⟨t, ht, h⟩ := metric.mem_nhds_iff.mp hs,
+  refine is_linear_map_real_of_bounded_nhds f (closed_ball_mem_nhds a $ half_pos ht) _,
+  replace h := (closed_ball_subset_ball $ half_lt_self ht).trans h,
+  rw real.closed_ball_eq_Icc at ⊢ h,
+  have ha :  a - t / 2 ≤ a + t / 2 := by linarith,
+  refine bounded_of_bdd_above_of_bdd_below (hf.map_bdd_above h _) (hf.map_bdd_below h _),
+  { refine ⟨a + t / 2, _, h $ right_mem_Icc.2 ha⟩,
+    rw upper_bounds_Icc ha,
+    exact left_mem_Ici },
+  { refine ⟨a - t / 2, _, h $ left_mem_Icc.2 ha⟩,
+    rw lower_bounds_Icc ha,
+    exact right_mem_Iic }
+end

src/analysis/normed/group/basic.lean

@@ -901,6 +901,16 @@ by rw [tendsto_uniformly_on_iff_tendsto_uniformly_on_filter,
     uniform_cauchy_seq_on_iff_uniform_cauchy_seq_on_filter,
     seminormed_group.uniform_cauchy_seq_on_filter_iff_tendsto_uniformly_on_filter_one]
 
+@[to_additive norm_nsmul_le] lemma norm_pow_le_mul_norm (n : ℕ) (a : E) : ‖a^n‖ ≤ n * ‖a‖ :=
+begin
+  induction n with n ih, { simp, },
+  simpa only [pow_succ', nat.cast_succ, add_mul, one_mul] using norm_mul_le_of_le ih le_rfl,
+end
+
+@[to_additive nnnorm_nsmul_le] lemma nnnorm_pow_le_mul_norm (n : ℕ) (a : E) : ‖a^n‖₊ ≤ n * ‖a‖₊ :=
+by simpa only [← nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_nat_cast]
+  using norm_pow_le_mul_norm n a
+
 end seminormed_group
 
 section induced
@@ -1047,16 +1057,6 @@ by { ext c,
   ((*) b) ⁻¹' sphere a r = sphere (a / b) r :=
 by { ext c, simp only [set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm] }
 
-@[to_additive norm_nsmul_le] lemma norm_pow_le_mul_norm (n : ℕ) (a : E) : ‖a^n‖ ≤ n * ‖a‖ :=
-begin
-  induction n with n ih, { simp, },
-  simpa only [pow_succ', nat.cast_succ, add_mul, one_mul] using norm_mul_le_of_le ih le_rfl,
-end
-
-@[to_additive nnnorm_nsmul_le] lemma nnnorm_pow_le_mul_norm (n : ℕ) (a : E) : ‖a^n‖₊ ≤ n * ‖a‖₊ :=
-by simpa only [← nnreal.coe_le_coe, nnreal.coe_mul, nnreal.coe_nat_cast]
-  using norm_pow_le_mul_norm n a
-
 @[to_additive] lemma pow_mem_closed_ball {n : ℕ} (h : a ∈ closed_ball b r) :
   a^n ∈ closed_ball (b^n) (n • r) :=
 begin

src/measure_theory/measure/lebesgue/eq_haar.lean

@@ -102,6 +102,29 @@ by { rw ← add_haar_measure_eq_volume_pi, apply_instance }
 
 namespace measure
 
+/-! ### Normed groups -/
+
+section seminormed_group
+variables {G : Type*} [measurable_space G] [group G] [topological_space G] [t2_space G]
+  [topological_group G] [borel_space G] [second_countable_topology G] [locally_compact_space G]
+variables {H : Type*} [measurable_space H] [seminormed_group H] [opens_measurable_space H]
+
+open metric
+
+@[to_additive]
+lemma _root_.measurable.exists_nhds_one_bounded (f : G →* H) (h : measurable f)
+  (μ : measure G . volume_tac) [μ.is_haar_measure] :
+  ∃ s, s ∈ 𝓝 (1 : G) ∧ bounded (f '' s) :=
+begin
+  obtain ⟨r, hr⟩ := exists_pos_preimage_ball f (1 : H) (ne_zero.ne μ),
+  refine ⟨_, div_mem_nhds_one_of_haar_pos μ (f ⁻¹' ball 1 r) (h measurable_set_ball) hr, _⟩,
+  rw image_div,
+  exact (bounded_ball.mono $ image_preimage_subset _ _).div
+    (bounded_ball.mono $ image_preimage_subset _ _),
+end
+
+end seminormed_group
+
 /-!
 ### Strict subspaces have zero measure
 -/

src/measure_theory/measure/measure_space.lean

@@ -2329,6 +2329,8 @@ by rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]
 @[simp] lemma ae_ne_bot : μ.ae.ne_bot ↔ μ ≠ 0 :=
 ne_bot_iff.trans (not_congr ae_eq_bot)
 
+instance ae_ne_bot.to_ne_zero [μ.ae.ne_bot] : ne_zero μ := ⟨ae_ne_bot.1 ‹_›⟩
+
 @[simp] lemma ae_zero {m0 : measurable_space α} : (0 : measure α).ae = ⊥ := ae_eq_bot.2 rfl
 
 @[mono] lemma ae_mono (h : μ ≤ ν) : μ.ae ≤ ν.ae := h.absolutely_continuous.ae_le

src/measure_theory/measure/open_pos.lean

@@ -58,6 +58,9 @@ measure_pos_of_nonempty_interior _ ⟨x, mem_interior_iff_mem_nhds.2 h⟩
 lemma is_open_pos_measure_smul {c : ℝ≥0∞} (h : c ≠ 0) : is_open_pos_measure (c • μ) :=
 ⟨λ U Uo Une, mul_ne_zero h (Uo.measure_ne_zero μ Une)⟩
 
+instance is_open_pos_measure.to_ae_ne_bot [nonempty X] : μ.ae.ne_bot :=
+ae_ne_bot.2 $ λ h, is_open_univ.measure_ne_zero μ univ_nonempty $ by rw [h, coe_zero, pi.zero_apply]
+
 variables {μ ν}
 
 protected lemma absolutely_continuous.is_open_pos_measure (h : μ ≪ ν) :