Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 02:06 f254c2f8

View on Github →

refactor(analysis/normed_space/{dual, pi_Lp}): split out inner product space parts (#9388) This is just moving code, no math changes. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/New.20folder.20analysis.2Finner_product_space

Estimated changes

Created src/analysis/inner_product_space/dual.lean

added def inner_product_space.isometric.to_dual

added theorem inner_product_space.ker_to_dual_map

added theorem inner_product_space.norm_to_dual'_apply

added theorem inner_product_space.norm_to_dual_apply

added theorem inner_product_space.norm_to_dual_map_apply

added theorem inner_product_space.norm_to_dual_symm_apply

added theorem inner_product_space.range_to_dual_map

added def inner_product_space.to_dual'

added theorem inner_product_space.to_dual'_apply

added theorem inner_product_space.to_dual'_isometry

added theorem inner_product_space.to_dual'_surjective

added def inner_product_space.to_dual

added theorem inner_product_space.to_dual_apply

added theorem inner_product_space.to_dual_eq_iff_eq'

added theorem inner_product_space.to_dual_eq_iff_eq

added def inner_product_space.to_dual_map

added theorem inner_product_space.to_dual_map_apply

added theorem inner_product_space.to_dual_map_eq_iff_eq

added theorem inner_product_space.to_dual_map_injective

added theorem inner_product_space.to_dual_map_isometry

Modified src/analysis/inner_product_space/euclidean_dist.lean

Created src/analysis/inner_product_space/pi_L2.lean

added def basis.isometry_euclidean_of_orthonormal

added def complex.isometry_euclidean

added theorem complex.isometry_euclidean_apply_one

added theorem complex.isometry_euclidean_apply_zero

added theorem complex.isometry_euclidean_proj_eq_self

added theorem complex.isometry_euclidean_symm_apply

added theorem euclidean_space.norm_eq

added def euclidean_space

added theorem finrank_euclidean_space

added theorem finrank_euclidean_space_fin

added def linear_isometry_equiv.from_orthogonal_span_singleton

added def linear_isometry_equiv.of_inner_product_space

added theorem pi_Lp.inner_apply

added theorem pi_Lp.norm_eq_of_L2

Modified src/analysis/normed_space/dual.lean

deleted def inner_product_space.isometric.to_dual

deleted theorem inner_product_space.ker_to_dual_map

deleted theorem inner_product_space.norm_to_dual'_apply

deleted theorem inner_product_space.norm_to_dual_apply

deleted theorem inner_product_space.norm_to_dual_map_apply

deleted theorem inner_product_space.norm_to_dual_symm_apply

deleted theorem inner_product_space.range_to_dual_map

deleted def inner_product_space.to_dual'

deleted theorem inner_product_space.to_dual'_apply

deleted theorem inner_product_space.to_dual'_isometry

deleted theorem inner_product_space.to_dual'_surjective

deleted def inner_product_space.to_dual

deleted theorem inner_product_space.to_dual_apply

deleted theorem inner_product_space.to_dual_eq_iff_eq'

deleted theorem inner_product_space.to_dual_eq_iff_eq

deleted def inner_product_space.to_dual_map

deleted theorem inner_product_space.to_dual_map_apply

deleted theorem inner_product_space.to_dual_map_eq_iff_eq

deleted theorem inner_product_space.to_dual_map_injective

deleted theorem inner_product_space.to_dual_map_isometry

Modified src/analysis/normed_space/pi_Lp.lean

deleted def basis.isometry_euclidean_of_orthonormal

deleted def complex.isometry_euclidean

deleted theorem complex.isometry_euclidean_apply_one

deleted theorem complex.isometry_euclidean_apply_zero

deleted theorem complex.isometry_euclidean_proj_eq_self

deleted theorem complex.isometry_euclidean_symm_apply

deleted theorem euclidean_space.norm_eq

deleted def euclidean_space

deleted theorem finrank_euclidean_space

deleted theorem finrank_euclidean_space_fin

deleted def linear_isometry_equiv.from_orthogonal_span_singleton

deleted def linear_isometry_equiv.of_inner_product_space

deleted theorem pi_Lp.inner_apply

deleted theorem pi_Lp.norm_eq_of_L2

Modified src/geometry/manifold/instances/real.lean

Modified src/measure_theory/function/conditional_expectation.lean