Commit 2022-09-07 15:10 62119451

View on Github →

feat(analysis/complex/upper_half_plane): Functions bounded at infinity (#15009) The defines the notion of functions on the upper half plane being bounded at infinity and zero at infinity. This is required for #13250.

Estimated changes

Created src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean

added def upper_half_plane.at_im_infty

added theorem upper_half_plane.at_im_infty_basis

added theorem upper_half_plane.at_im_infty_mem

added def upper_half_plane.bounded_at_im_infty_subalgebra

added theorem upper_half_plane.bounded_mem

added def upper_half_plane.is_bounded_at_im_infty

added def upper_half_plane.is_zero_at_im_infty

added theorem upper_half_plane.prod_of_bounded_is_bounded

added theorem upper_half_plane.zero_at_im_infty

added def upper_half_plane.zero_at_im_infty_submodule

added theorem upper_half_plane.zero_form_is_bounded_at_im_infty

Created src/order/filter/zero_and_bounded_at_filter.lean

added def filter.bounded_at_filter

added def filter.bounded_filter_subalgebra

added def filter.bounded_filter_submodule

added def filter.zero_at_filter

added def filter.zero_at_filter_add_submonoid

added theorem filter.zero_at_filter_is_bounded_at_filter

added def filter.zero_at_filter_submodule

added theorem filter.zero_is_bounded_at_filter

added theorem filter.zero_is_zero_at_filter