Commit 2022-06-10 10:43 95da6493

View on Github →

feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379) The generalisation is to allow a family of vectors indexed by a general indexing set ι (carrying appropriate order typeclasses) rather than just ℕ.

Estimated changes

Modified src/analysis/box_integral/partition/basic.lean

Modified src/analysis/box_integral/partition/tagged.lean

Modified src/analysis/inner_product_space/gram_schmidt_ortho.lean

modified theorem gram_schmidt_def'

modified theorem gram_schmidt_def

deleted theorem gram_schmidt_ne_zero'

modified theorem gram_schmidt_ne_zero

added theorem gram_schmidt_ne_zero_coe

deleted theorem gram_schmidt_normed_unit_length'

modified theorem gram_schmidt_normed_unit_length

added theorem gram_schmidt_normed_unit_length_coe

modified theorem gram_schmidt_orthogonal

modified theorem gram_schmidt_orthonormal

modified theorem gram_schmidt_pairwise_orthogonal

modified theorem gram_schmidt_zero

modified theorem span_gram_schmidt

Modified src/data/finset/lattice.lean

deleted theorem finset.sup_le_iff

Modified src/data/finset/powerset.lean

Modified src/order/rel_classes.lean

added def is_well_order.to_has_well_founded

Modified src/order/succ_pred/basic.lean

added theorem order.Ioi_pred_eq_insert_of_not_is_min