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

MantasBaksys · 2022-03-25T15:46:10Z

Cauchy's functional equation over the real-line for a Lebesgue measurable function and some of the usual variants from which linearity of a given function is deduced.

depends on: [Merged by Bors] - feat(topology/algebra/group): add small topology lemma #12931
depends on: [Merged by Bors] - feat(measure_theory/measure/haar): Add the Steinhaus Theorem #12932
depends on: [Merged by Bors] - feat(order/bounds): Boundedness of monotone/antitone functions #13079
depends on: [Merged by Bors] - feat(analysis/normed_space/pointwise): Addition of balls #13381
depends on: [Merged by Bors] - feat({data/{finset,set},order/filter}/pointwise): More lemmas #14216

…-Equation

…tion

…-Equation

urkud

Thank you for working on this! The proof can be golfed a lot using lemmas I mention in my comments.

urkud · 2022-05-29T13:37:14Z

src/analysis/cauchy_equation.lean

+
+/-- **Cauchy's functional equation**. An additive monoid homomorphism automatically preserves `ℚ`.
+-/
+theorem add_monoid_hom.is_linear_map_rat (f : ℝ →+ ℝ) : is_linear_map ℚ f :=


See also add_monoid_hom.to_rat_linear_map

See #12933 (comment)

src/analysis/cauchy_equation.lean

…sitive measure (#14449) Motivated by #12933 Co-authored-by: Mantas Bakšys <baksysmantas@gmail.com>

…-Equation

…sitive measure (#14449) Motivated by #12933 Co-authored-by: Mantas Bakšys <baksysmantas@gmail.com>

src/analysis/cauchy_equation.lean

urkud · 2022-06-11T14:29:10Z

src/analysis/cauchy_equation.lean

+λ h, is_open_univ.measure_ne_zero μ univ_nonempty $ by rw [h, coe_zero, pi.zero_apply]
+
+lemma exists_zero_nhds_bounded (f : ℝ →+ ℝ) (h : measurable f) :
+  ∃ s, s ∈ 𝓝 (0 : ℝ) ∧ bounded (f '' s) :=


What is the right generality for this lemma? Probably, it's true at least for all finite dimensional real normed spaces.

urkud · 2022-06-11T14:40:11Z

src/analysis/cauchy_equation.lean

+end
+
+lemma additive_continuous_at_zero_of_bounded_nhds_zero (f : ℝ →+ ℝ) (hs : s ∈ 𝓝 (0 : ℝ))
+  (hbounded : bounded (f '' s)) : continuous_at f 0 :=


If you upgrade f to a ℚ-linear map, then you can use linear_map.bound_of_shell or linear_map.bound_of_ball_bound. Again, you can upgrade your lemma to a real TVS.

urkud · 2022-06-11T14:41:38Z

src/analysis/cauchy_equation.lean

+  { 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 :=


This lemma and most lemmas below are already in mathlib, aren't they?

…-Equation

eric-wieser · 2023-07-16T15:26:18Z

@YaelDillies, are you interested in finishing this, or are your own PRs more important to you?

YaelDillies · 2023-07-16T18:47:43Z

Yes, I in fact started fixing it earlier today. It needs some more cleanup but the gist is here.

urkud · 2023-09-10T17:45:25Z

src/analysis/cauchy_equation.lean

+
+local notation `ℝⁿ` := ι → ℝ
+
+lemma add_monoid_hom.measurable_of_continuous (f : ℝ →+ ℝ) (h : measurable f) : continuous f :=


Name says measurable_of_continuous but the theorem says measurable f -> continuous f.

urkud · 2023-09-10T17:46:21Z

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 ‹_›⟩


We have [NeZero μ] : μ.ae.NeBot in Lean 4.

urkud · 2023-09-10T17:57:34Z

src/analysis/cauchy_equation.lean

+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))


Isn't [is_R_or_C H] too strong? Is it true for any normed space over rationals?

YaelDillies · 2023-11-18T11:19:22Z

Ported to LeanCamCombi

MantasBaksys and others added 13 commits March 21, 2022 14:56

testing

63139ef

update

b675fb1

reduce imports

8ceb0a4

steinhaus to prove

bebb1aa

blueprint

c6dd872

update

0a7f643

Merge remote-tracking branch 'origin/master' into Cauchy's-Functional…

0d9d525

…-Equation

finish steinhaus_theorem

e2aba3c

update and add variants

28c3450

update

c49f525

fix line length

44409e5

remove overhead + add steinhaus_theorem

128c15c

bring back cauchy

207fbe9

MantasBaksys added the WIP Work in progress label Mar 25, 2022

leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 25, 2022

MantasBaksys changed the title ~~Cauchy's functional equation~~ feat (analysis/cauchy_equation) : Add Cauchy's Functional Equation Mar 25, 2022

MantasBaksys added 14 commits March 25, 2022 19:25

replace occurences

158c04b

fix typos

7d6de09

Merge branch 'mantas-small-lemma' into mantas-steinhaus-theorem

1257029

update proofs and statements

e5d8c67

fix dependency

b82bf8f

Merge remote-tracking branch 'origin/master' into mantas-small-lemma

1593475

segment into lemmas + golf

29475c1

Merge branch 'mantas-small-lemma' into mantas-steinhaus-theorem

d4693d1

fix lint

d9c3d89

Merge branch 'mantas-small-lemma' into mantas-steinhaus-theorem

64c8e5c

truly fix lint

17940fc

fix errors

5cd4d99

Merge branch 'mantas-steinhaus-theorem' into Cauchy's-Functional-Equa…

635b89a

…tion

make compile

50b9884

YaelDillies added 2 commits May 29, 2022 01:30

Merge remote-tracking branch 'origin/master' into Cauchy's-Functional…

b23ea5c

…-Equation

bump, golf

47cdea2

YaelDillies added RFC Request for comment and removed WIP Work in progress labels May 29, 2022

urkud mentioned this pull request May 29, 2022

[Merged by Bors] - feat(measure_theory/measure/measure_space): there exists a ball of positive measure #14449

Closed

urkud reviewed May 29, 2022

View reviewed changes

kill continuous.is_linear_real

5328524

bors bot pushed a commit that referenced this pull request Jun 4, 2022

feat(measure_theory/measure/measure_space): there exists a ball of po…

b5973ba

…sitive measure (#14449) Motivated by #12933 Co-authored-by: Mantas Bakšys <baksysmantas@gmail.com>

YaelDillies added 2 commits June 5, 2022 14:07

Merge remote-tracking branch 'origin/master' into Cauchy's-Functional…

43948c7

…-Equation

bump

eb6b1e8

tomaz1502 pushed a commit that referenced this pull request Jun 5, 2022

feat(measure_theory/measure/measure_space): there exists a ball of po…

94ff106

…sitive measure (#14449) Motivated by #12933 Co-authored-by: Mantas Bakšys <baksysmantas@gmail.com>

more bump

1e0e02b

urkud reviewed Jun 11, 2022

View reviewed changes

Merge remote-tracking branch 'origin/master' into Cauchy's-Functional…

92817ed

…-Equation

move is_open_pos_measure.to_ae_ne_bot

c17cdc9

YaelDillies requested a review from a team as a code owner July 16, 2023 18:47

github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jul 16, 2023

YaelDillies added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 16, 2023

semorrison added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 16, 2023

YaelDillies added 2 commits August 3, 2023 08:15

fix build, generalise more

6b4eb9d

move ae_ne_bot.to_ne_zero

a937abb

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 3, 2023

urkud reviewed Sep 10, 2023

View reviewed changes

YaelDillies closed this Nov 18, 2023

YaelDillies deleted the Cauchy's-Functional-Equation branch November 18, 2023 11:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

MantasBaksys commented Mar 25, 2022 •

edited by github-actions bot

urkud left a comment

urkud May 29, 2022

YaelDillies May 29, 2022

urkud Jun 11, 2022

urkud Jun 11, 2022

urkud Jun 11, 2022

eric-wieser commented Jul 16, 2023

YaelDillies commented Jul 16, 2023

urkud Sep 10, 2023

urkud Sep 10, 2023

urkud Sep 10, 2023

YaelDillies commented Nov 18, 2023


		local notation `ℝⁿ` := ι → ℝ

		lemma add_monoid_hom.measurable_of_continuous (f : ℝ →+ ℝ) (h : measurable f) : continuous f :=

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

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

Conversation

MantasBaksys commented Mar 25, 2022 • edited by github-actions bot

urkud left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser commented Jul 16, 2023

YaelDillies commented Jul 16, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

YaelDillies commented Nov 18, 2023

MantasBaksys commented Mar 25, 2022 •

edited by github-actions bot