chore(analysis/inner_product_space): remove two redundant definitions (again) #19058
Conversation
mcdoll
added
awaiting-review
| @@ -60,10 +60,14 @@ variables [normed_add_comm_group V] [measurable_space V] [borel_space V] | |||
| lemma fourier_integrand_integrable (w : V) : | |||
| integrable f ↔ integrable (λ v : V, e [-⟪v, w⟫] • f v) := | |||
| begin | |||
| have hL : continuous (λ p : V × V, bilin_form_of_real_inner.to_lin p.1 p.2) := continuous_inner, | |||
| have hL : continuous (λ p : V × V, innerₛₗ ℝ p.1 p.2) := continuous_inner, | |||
| -- TODO: remove the continuity assumption from `vector_fourier.fourier_integral_convergent_iff` | |||
There was a problem hiding this comment.
I don't think the lemma is still true without this assumption, as you can get measurability issues, no?
There was a problem hiding this comment.
I haven't checked the details, but I agree that one probably has to assume measurability.
|
|
||
| /-- The real inner product as a bilinear form. -/ | ||
| @[simps] | ||
| def bilin_form_of_real_inner : bilin_form ℝ F := |
There was a problem hiding this comment.
I need this definition in a downstream project. What am I supposed to use instead if you're removing it?
(I agree with the removal of sesq_form_of_inner as it has an easy replacement)
There was a problem hiding this comment.
@eric-wieser Can you point us to the downstream project?
There was a problem hiding this comment.
It's important to me that these terms are of the form bilin_form.to_quadratic_form B, as that's the language used when working with clifford_algebra.change_form_equiv.
In the long run I agree it makes sense to remove this def; but in the short term, the quadratic_form API is very bilin_form-centric, and I don't think we should be deleting bilin_form API until we've finished refactoring quadratic_form.
There was a problem hiding this comment.
Can't you just add bilin_form_of_real_inner in that project? As you can see if we keep the definition in mathlib, then it gets used in places where we have better things.
There was a problem hiding this comment.
Can't you just add
bilin_form_of_real_innerin that project?
Yes, but I don't see why I should need to. Until bilin_form is deprecated / made an abbreviation, I don't see what we gain by removing parts of its API.
As you can see if we keep the definition in mathlib, then it gets used in places where we have better things.
I think a better solution would be to either:
- Edit the docstring to mention
innerₛₗ ℝ : F →ₗ⋆[ℝ] F →ₗ[ℝ] ℝas an alternative tobilin_form_of_real_inner : bilin_form ℝ F - Add a simp-lemma that says
bilin_form_of_real_inner.to_lin = innerₛₗ ℝ(proof should beext, refl)
Mathlib is full of non-simp-normal bundlings; the way we indicate that they should not be used unless the specific bundling is needed is by simping them away and adding docstrings.
There was a problem hiding this comment.
I consider bilin_form deprecated. Would you be happy with adding
namespace linear_map
variables [comm_semiring R] [add_comm_monoid M] [module R M]
def to_quadratic_form (B : M →ₗ[R] M →ₗ[R] R) : quadratic_form R M :=
B.to_bilin.to_quadratic_form
@[simp] lemma to_quadratic_form_apply (B : M →ₗ[R] M →ₗ[R] R) (x : M) :
B.to_quadratic_form x = B x x :=
rfl
end linear_mapto the quadratic form file?
There was a problem hiding this comment.
Those 10 lines aren't a substitute for the 70 lines of API lemmas here, and the handful of API lemmas spread around the file.
Why don't we just leave the definition around until mathlib4, and tag it @[deprecated] there? This file is on the critical porting path now; and I'd strongly prefer the frozen version in mathlib3 not be one that doesn't work in my project.
I don't think there's any urgency to delete it, and the other changes in this PR look good to me.
github-actions
bot
removed
the
awaiting-CI
eric-wieser
added
awaiting-author
|
|
||
| @[simp] lemma innerₛₗ_apply (v w : E) : innerₛₗ 𝕜 v w = ⟪v, w⟫ := rfl | ||
|
|
||
| variables {𝕜} |
There was a problem hiding this comment.
| variables {𝕜} | |
| variables {𝕜} | |
| /-- The real inner product as a bilinear form. -/ | |
| @[simps] | |
| def bilin_form_of_real_inner : bilin_form ℝ F := | |
| { bilin := inner, | |
| bilin_add_left := inner_add_left, | |
| bilin_smul_left := λ a x y, inner_smul_left _ _ _, | |
| bilin_add_right := inner_add_right, | |
| bilin_smul_right := λ a x y, inner_smul_right _ _ _ } | |
| @[simp] | |
| lemma bilin_form_of_real_inner_to_lin : (bilin_form_of_real_inner : bilin_form ℝ F).to_lin = innerₛₗ ℝ := rfl |
as discussed above
This PR removes
sesq_form_of_innerandbilin_form_of_real_inner. The former one is just(innerₛₗ 𝕜).flipand the later one can be easily replaced byinnerₛₗ 𝕜. The definitionbilin_form_of_real_innerwas earlier removed in #15780, but then restored in #18093. Since then nothing has been added to mathlib that makesbilin_form_of_real_innernecessary. In particular the mentioned quadratic form is just the square of the norm.We also generalize
bilin_form_of_real_inner_orthogonaland the two versions ofis_adjoint_pair_innerso that they hold for complex inner products and not just the reals.Add a few comments for a proof in the Riemann-Lebesgue lemma which is unnecessarily complicated, but fixing this is not in the scope of this PR.