[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210

RemyDegenne · 2021-07-06T07:01:26Z

src/measure_theory/lp_space.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser · 2021-07-06T09:59:00Z

src/measure_theory/lp_space.lean

+variables {𝕜 : Type*} [is_R_or_C 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F]

-/-- Composing `f : Lp ` with `L : E →L[ℝ] F`. -/
-def comp_Lp (L : E →L[ℝ] F) (f : Lp E p μ) : Lp F p μ :=
+/-- Composing `f : Lp ` with `L : E →L[𝕜] F`. -/
+def comp_Lp (L : E →L[𝕜] F) (f : Lp E p μ) : Lp F p μ :=
 L.lipschitz.comp_Lp (map_zero L) f


What actually needs is_R_or_C here? Is [nondiscrete_normed_field 𝕜] enough?

This def and the two lemmas below it are true for only

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [semi_normed_space 𝕜 E] [semi_normed_space 𝕜 F]

while the rest of this section is true for

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F]

I think you can replace every occurence of normed_space in this file with semi_normed_space which means you don't need the second set of assumptions to be different.

Indeed all those hypotheses can be relaxed. This is code I wrote before all the normed_space in mathlib became semi_normed_space.
I'll add semi_ to all hypotheses in the file (if that works).

It worked without any issue.

It's more complicated in the set_integral file. Either some normed_space in other files should be replaced by semi_normed_space, or most normed_space arguments are actually needed.

Perhaps the normed_group arguments need to be replaced by semi_normed_group? Just a thought, I haven't tested it.

Right, I replaced some normed_space by semi_normed_space, but those are all still normed_group (and changing to semi_normed_group looks like it causes errors). So I effectively still have normed_space and it is as if I did not do anything. I suppose the two main possible courses of action are to keep things as they are here, or to work towards using semi_normed_group as much as possible.

I confess that investigating that normed vs seminormed issue in all Lp/integral files does not interest me very much right now, and I think that it is beyond the goal of this PR.

I confess that investigating that normed vs seminormed issue in all Lp/integral files does not interest me very much right now

I agree!

Sorry for sending you into that rabbit hole - I only meant it as a throwaway observation, the change to nondiscrete_normed_field was much more relevant.

…ib into integral_comp

This reverts commit e8f80d2.

RemyDegenne · 2021-07-07T14:03:49Z

I undid all the semi_normed_group related changes to bring this PR back to its original goal: extend some lemmas about linear map from R to is_R_or_C (or nondiscrete_normed_field when it is sufficient).
It is now ready for review.

hrmacbeth

LGTM, thanks!

hrmacbeth · 2021-07-07T17:56:24Z

src/measure_theory/lp_space.lean

 `Lp E p μ`. -/
-def comp_LpL [fact (1 ≤ p)] (L : E →L[ℝ] F) : (Lp E p μ) →L[ℝ] (Lp F p μ) :=
+def comp_LpL [fact (1 ≤ p)] (L : E →L[𝕜] F) : (Lp E p μ) →L[𝕜] (Lp F p μ) :=


Constructions like this are often hard to find in mathlib, because you don't think about them until you need them. While you're working here, would you mind adding a cross-reference to the similar constructions continuous_linear_map.comp_left_continuous, continuous_linear_map.comp_left_continuous_bounded, just to increase visibility?

Done!
Doing so, I realized that I did not know what comp_LpL was. It was in the same section as a lemma I wanted to generalize, so it got the same treatment, but I did not even read it.

hrmacbeth

Thanks!

bors d+

src/measure_theory/lp_space.lean

bors · 2021-07-11T18:56:24Z

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

RemyDegenne · 2021-07-11T19:41:32Z

bors r+

…s from R to is_R_or_C (#8210) Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>

bors · 2021-07-11T20:46:07Z

Pull request successfully merged into master.

Build succeeded:

RemyDegenne added 2 commits July 6, 2021 08:54

extend integral comp lemmas

be00f14

add space

5495f8e

RemyDegenne added awaiting-review The author would like community review of the PR awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 6, 2021

undo accidental deletion of integral_apply

c354445

fix

81dd754

RemyDegenne added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 6, 2021

eric-wieser reviewed Jul 6, 2021

View reviewed changes

src/measure_theory/lp_space.lean Outdated Show resolved Hide resolved

Update docstring

fd532ea

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser reviewed Jul 6, 2021

View reviewed changes

RemyDegenne added 2 commits July 6, 2021 12:05

use nondiscrete_normed_field

603a922

Merge branch 'integral_comp' of github.com:leanprover-community/mathl…

9aca324

…ib into integral_comp

RemyDegenne added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 6, 2021

use semi_normed_space

30dddea

RemyDegenne added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 6, 2021

RemyDegenne added 6 commits July 6, 2021 12:17

use semi_normed_space

e8f80d2

Revert "use semi_normed_space"

897f5b7

This reverts commit e8f80d2.

add one semi_

67e010f

use more semi_normed_space

c6f7218

use semi_normed_group

3abe826

distinguish normed and semi_normed in lp_space

5cefb13

RemyDegenne removed the awaiting-review The author would like community review of the PR label Jul 6, 2021

RemyDegenne added 13 commits July 7, 2021 09:58

undo l1_space

7dd7bf6

undo set_integral

073c244

undo simple_func_dense

46f2a02

undo bounded and compact

9e40657

undo gromov_hausdorff

6722134

fake commit

762c3cd

fake commit

a01130f

Merge remote-tracking branch 'origin/master' into integral_comp

f31481c

remove semi_ in lp_space

d76e2c3

remove primes in lp_space

533290e

more undo in lp_space

2185b53

undo

5103d1b

undo bounded

bb533c9

RemyDegenne added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jul 7, 2021

hrmacbeth reviewed Jul 7, 2021

View reviewed changes

add references in docstring

56372a4

RemyDegenne mentioned this pull request Jul 8, 2021

[Merged by Bors] - feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral #8229

Closed

1 task

hrmacbeth reviewed Jul 11, 2021

View reviewed changes

src/measure_theory/lp_space.lean Outdated Show resolved Hide resolved

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 11, 2021

Update src/measure_theory/lp_space.lean

d418652

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

bors bot pushed a commit that referenced this pull request Jul 11, 2021

feat(measure_theory/{lp_space,set_integral}): extend linear map lemma…

19beb12

…s from R to is_R_or_C (#8210) Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>

bors bot changed the title ~~feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C~~ [Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C Jul 11, 2021

bors bot closed this Jul 11, 2021

bors bot deleted the integral_comp branch July 11, 2021 20:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210

[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210

RemyDegenne commented Jul 6, 2021 •

edited

eric-wieser Jul 6, 2021

eric-wieser Jul 6, 2021 •

edited

RemyDegenne Jul 6, 2021

RemyDegenne Jul 6, 2021

RemyDegenne Jul 6, 2021

hrmacbeth Jul 6, 2021

RemyDegenne Jul 6, 2021

hrmacbeth Jul 6, 2021 •

edited

eric-wieser Jul 8, 2021

RemyDegenne commented Jul 7, 2021

hrmacbeth left a comment

hrmacbeth Jul 7, 2021

RemyDegenne Jul 7, 2021

hrmacbeth left a comment

bors bot commented Jul 11, 2021

RemyDegenne commented Jul 11, 2021

bors bot commented Jul 11, 2021

[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210

[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210

Conversation

RemyDegenne commented Jul 6, 2021 • edited

Choose a reason for hiding this comment

eric-wieser Jul 6, 2021 • edited

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

hrmacbeth Jul 6, 2021 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RemyDegenne commented Jul 7, 2021

hrmacbeth left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hrmacbeth left a comment

Choose a reason for hiding this comment

bors bot commented Jul 11, 2021

RemyDegenne commented Jul 11, 2021

bors bot commented Jul 11, 2021

RemyDegenne commented Jul 6, 2021 •

edited

eric-wieser Jul 6, 2021 •

edited

hrmacbeth Jul 6, 2021 •

edited