-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C #8210
Changes from 5 commits
be00f14
5495f8e
c354445
81dd754
fd532ea
603a922
9aca324
30dddea
e8f80d2
897f5b7
67e010f
c6f7218
3abe826
5cefb13
af62add
4756a3a
5bce86a
da9fc10
4d16fed
e6a45f5
b66ca78
5300fa3
0ef8151
9acee35
1920f24
619507e
7dd7bf6
073c244
46f2a02
9e40657
6722134
762c3cd
a01130f
f31481c
d76e2c3
533290e
2185b53
5103d1b
bb533c9
56372a4
d418652
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -1540,19 +1540,23 @@ lemma continuous_comp_Lp [fact (1 ≤ p)] (hg : lipschitz_with c g) (g0 : g 0 = | |
end lipschitz_with | ||
|
||
namespace continuous_linear_map | ||
variables [normed_space ℝ E] [normed_space ℝ F] | ||
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 | ||
|
||
lemma coe_fn_comp_Lp (L : E →L[ℝ] F) (f : Lp E p μ) : | ||
lemma coe_fn_comp_Lp (L : E →L[𝕜] F) (f : Lp E p μ) : | ||
∀ᵐ a ∂μ, (L.comp_Lp f) a = L (f a) := | ||
lipschitz_with.coe_fn_comp_Lp _ _ _ | ||
|
||
variables (μ p) | ||
/-- Composing `f : Lp E p μ` with `L : E →L[ℝ] F`, seen as a `ℝ`-linear map on `Lp E p μ`. -/ | ||
def comp_Lpₗ (L : E →L[ℝ] F) : (Lp E p μ) →ₗ[ℝ] (Lp F p μ) := | ||
lemma norm_comp_Lp_le (L : E →L[𝕜] F) (f : Lp E p μ) : ∥L.comp_Lp f∥ ≤ ∥L∥ * ∥f∥ := | ||
lipschitz_with.norm_comp_Lp_le _ _ _ | ||
|
||
variables (μ p) [measurable_space 𝕜] [opens_measurable_space 𝕜] | ||
|
||
/-- Composing `f : Lp E p μ` with `L : E →L[𝕜] F`, seen as a `𝕜`-linear map on `Lp E p μ`. -/ | ||
def comp_Lpₗ (L : E →L[𝕜] F) : (Lp E p μ) →ₗ[𝕜] (Lp F p μ) := | ||
{ to_fun := λ f, L.comp_Lp f, | ||
map_add' := begin | ||
intros f g, | ||
|
@@ -1571,18 +1575,12 @@ def comp_Lpₗ (L : E →L[ℝ] F) : (Lp E p μ) →ₗ[ℝ] (Lp F p μ) := | |
simp only [ha1, ha2, ha3, ha4, map_smul, pi.smul_apply], | ||
end } | ||
|
||
variables {μ p} | ||
lemma norm_comp_Lp_le (L : E →L[ℝ] F) (f : Lp E p μ) : ∥L.comp_Lp f∥ ≤ ∥L∥ * ∥f∥ := | ||
lipschitz_with.norm_comp_Lp_le _ _ _ | ||
|
||
variables (μ p) | ||
|
||
/-- Composing `f : Lp E p μ` with `L : E →L[ℝ] F`, seen as a continuous `ℝ`-linear map on | ||
/-- Composing `f : Lp E p μ` with `L : E →L[𝕜] F`, seen as a continuous `𝕜`-linear map on | ||
`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 μ) := | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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 There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done! |
||
linear_map.mk_continuous (L.comp_Lpₗ p μ) ∥L∥ L.norm_comp_Lp_le | ||
|
||
lemma norm_compLpL_le [fact (1 ≤ p)] (L : E →L[ℝ] F) : | ||
lemma norm_compLpL_le [fact (1 ≤ p)] (L : E →L[𝕜] F) : | ||
∥L.comp_LpL p μ∥ ≤ ∥L∥ := | ||
linear_map.mk_continuous_norm_le _ (norm_nonneg _) _ | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What actually needs
is_R_or_C
here? Is[nondiscrete_normed_field 𝕜]
enough?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This def and the two lemmas below it are true for only
while the rest of this section is true for
I think you can replace every occurence of
normed_space
in this file withsemi_normed_space
which means you don't need the second set of assumptions to be different.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indeed all those hypotheses can be relaxed. This is code I wrote before all the
normed_space
in mathlib becamesemi_normed_space
.I'll add
semi_
to all hypotheses in the file (if that works).There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It worked without any issue.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's more complicated in the set_integral file. Either some
normed_space
in other files should be replaced bysemi_normed_space
, or mostnormed_space
arguments are actually needed.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Perhaps the
normed_group
arguments need to be replaced bysemi_normed_group
? Just a thought, I haven't tested it.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Right, I replaced some
normed_space
bysemi_normed_space
, but those are all stillnormed_group
(and changing tosemi_normed_group
looks like it causes errors). So I effectively still havenormed_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 usingsemi_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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.