Commit 2023-05-25 17:58 fea3e4ca

View on Github →

feat: port Analysis.InnerProductSpace.Basic (#4280) I had to add big maxHeartbeats increases into two places, but I haven't been able to improve the situation (it compiles though). This might need to be addressed before merging.

Estimated changes

added theorem Continuous.inner
added theorem ContinuousAt.inner
added theorem ContinuousOn.inner
added theorem Dfinsupp.inner_sum
added theorem Dfinsupp.sum_inner
added theorem Filter.Tendsto.inner
added theorem Finsupp.inner_sum
added theorem Finsupp.sum_inner
added structure InnerProductSpace.Core
added theorem IsROrC.inner_apply
added theorem OrthogonalFamily.comp
added def OrthogonalFamily
added theorem Orthonormal.comp
added theorem Orthonormal.equiv_refl
added theorem Orthonormal.equiv_symm
added theorem Orthonormal.inner_sum
added theorem Orthonormal.map_equiv
added theorem Orthonormal.ne_zero
added def Orthonormal
added theorem Submodule.coe_inner
added theorem abs_real_inner_le_norm
added theorem continuous_inner
added theorem dist_div_norm_sq_smul
added theorem ext_inner_left
added theorem ext_inner_map
added theorem ext_inner_right
added def innerSL
added def innerSLFlip
added theorem innerSLFlip_apply
added theorem innerSL_apply
added theorem innerSL_apply_coe
added theorem innerSL_apply_norm
added theorem inner_add_add_self
added theorem inner_add_left
added theorem inner_add_right
added theorem inner_conj_symm
added theorem inner_eq_norm_mul_iff
added theorem inner_eq_zero_symm
added theorem inner_im_symm
added theorem inner_map_complex
added theorem inner_map_polarization
added theorem inner_map_self_eq_zero
added theorem inner_neg_left
added theorem inner_neg_neg
added theorem inner_neg_right
added theorem inner_re_symm
added theorem inner_re_zero_left
added theorem inner_re_zero_right
added theorem inner_self_conj
added theorem inner_self_eq_norm_sq
added theorem inner_self_eq_zero
added theorem inner_self_im
added theorem inner_self_ne_zero
added theorem inner_self_nonneg
added theorem inner_self_nonpos
added theorem inner_self_ofReal_norm
added theorem inner_self_ofReal_re
added theorem inner_self_re_eq_norm
added theorem inner_smul_left
added theorem inner_smul_real_left
added theorem inner_smul_real_right
added theorem inner_smul_right
added theorem inner_sub_left
added theorem inner_sub_right
added theorem inner_sub_sub_self
added theorem inner_sum
added theorem inner_zero_left
added theorem inner_zero_right
added def innerₛₗ
added theorem innerₛₗ_apply
added theorem innerₛₗ_apply_coe
added theorem nnnorm_inner_le_nnnorm
added theorem norm_add_mul_self
added theorem norm_add_mul_self_real
added theorem norm_add_sq
added theorem norm_add_sq_real
added theorem norm_eq_sqrt_inner
added theorem norm_inner_eq_norm_iff
added theorem norm_inner_le_norm
added theorem norm_inner_symm
added theorem norm_sub_eq_norm_add
added theorem norm_sub_mul_self
added theorem norm_sub_mul_self_real
added theorem norm_sub_sq
added theorem norm_sub_sq_real
added theorem orthonormal_empty
added theorem orthonormal_iff_ite
added theorem orthonormal_span
added theorem parallelogram_law
added theorem re_inner_le_norm
added theorem real_inner_I_smul_self
added theorem real_inner_comm
added theorem real_inner_eq_re_inner
added theorem real_inner_le_norm
added theorem real_inner_self_abs
added theorem real_inner_self_nonneg
added theorem real_inner_self_nonpos
added theorem real_inner_smul_left
added theorem real_inner_smul_right
added def sesqFormOfInner
added theorem sum_inner