Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(measure_theory/l2_space): L2 is an inner product space #6596

Closed
wants to merge 79 commits into from
Closed

[Merged by Bors] - feat(measure_theory/l2_space): L2 is an inner product space #6596

wants to merge 79 commits into from

Commits on Mar 8, 2021

  1. prove that l2 is an inner_product_space

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    b2e2b05 View commit details
    Browse the repository at this point in the history

  2. move lemmas to their files

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    5fb9cd3 View commit details
    Browse the repository at this point in the history

  3. move lemmas

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    2be7013 View commit details
    Browse the repository at this point in the history

  4. move ae_measurable.inner

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    42aae48 View commit details
    Browse the repository at this point in the history

  5. relax hypotheses of snorm'_norm_rpow

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    51d51bc View commit details
    Browse the repository at this point in the history

  6. relax hypotheses of snorm_norm_rpow

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    b6b5096 View commit details
    Browse the repository at this point in the history

  7. start conversion to is_R_or_C

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    1eb530e View commit details
    Browse the repository at this point in the history

  8. fix type

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    817c7dc View commit details
    Browse the repository at this point in the history

  9. more is_R_or_C

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    27d3b46 View commit details
    Browse the repository at this point in the history

  10. remove comment

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    c2207dd View commit details
    Browse the repository at this point in the history

  11. remove duplicate lemma

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    29315d0 View commit details
    Browse the repository at this point in the history

  12. fix error by adding 'real' section

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    57def92 View commit details
    Browse the repository at this point in the history

  13. prove integral_smul for more that R

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    b2f92ad View commit details
    Browse the repository at this point in the history

  14. remove a lemma

    @RemyDegenne
    RemyDegenne committed Mar 8, 2021
    Configuration menu
    Copy the full SHA
    04fdee7 View commit details
    Browse the repository at this point in the history

Commits on Mar 9, 2021

  1. change snorm_norm_rpow

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    fc16998 View commit details
    Browse the repository at this point in the history

  2. shorten proofs of add_left and smul_left

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    20cef34 View commit details
    Browse the repository at this point in the history

  3. integral of a composition with clm

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    7c3b693 View commit details
    Browse the repository at this point in the history

  4. add lintegral_conj and lintegral_coe_is_R_or_C

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    8bae6fe View commit details
    Browse the repository at this point in the history

  5. write conj_smul lemma with a sorry

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    731a80f View commit details
    Browse the repository at this point in the history

  6. only two sorry left, for non-integrable cases

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    29bad52 View commit details
    Browse the repository at this point in the history

  7. composition with a continuous_linear_equiv

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    7f983e5 View commit details
    Browse the repository at this point in the history

  8. work on composition with linear map

    @sgouezel
    sgouezel committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    43a04d4 View commit details
    Browse the repository at this point in the history

  9. merge upstream

    @sgouezel
    sgouezel committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    e608a7c View commit details
    Browse the repository at this point in the history

  10. remove some of the useless linear composition stuff

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    dac8f54 View commit details
    Browse the repository at this point in the history

  11. remove integral_linear_map

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    2455b71 View commit details
    Browse the repository at this point in the history

  12. move lemmas from integration to is_R_or_C

    @RemyDegenne
    RemyDegenne committed Mar 9, 2021
    Configuration menu
    Copy the full SHA
    6afeb40 View commit details
    Browse the repository at this point in the history

Commits on Mar 10, 2021

  1. mimic complex api for linear maps

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    7b062d0 View commit details
    Browse the repository at this point in the history

  2. propagate name changes

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    bb21420 View commit details
    Browse the repository at this point in the history

  3. move snorm_norm_rpow

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    5995b12 View commit details
    Browse the repository at this point in the history

  4. use inner notation

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    4cc25ac View commit details
    Browse the repository at this point in the history

  5. add docstring to bochner_integration, pointing to set_integral

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    3badda9 View commit details
    Browse the repository at this point in the history

  6. remove line breaks

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    c83a0c3 View commit details
    Browse the repository at this point in the history

  7. rewrite docstring

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    4e0cedf View commit details
    Browse the repository at this point in the history

  8. add snorm_inner_lt_top

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    7aaa48e View commit details
    Browse the repository at this point in the history

  9. minor

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    b936e7d View commit details
    Browse the repository at this point in the history

  10. change names in complex to match is_R_or_C

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    7752fda View commit details
    Browse the repository at this point in the history

  11. fix lint errors

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    aa809a3 View commit details
    Browse the repository at this point in the history

  12. fix lint errors

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    176f539 View commit details
    Browse the repository at this point in the history

  13. change complex.basic docstring

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    0895277 View commit details
    Browse the repository at this point in the history

  14. of_real_bit0

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    a42a349 View commit details
    Browse the repository at this point in the history

  15. remove space

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    84c603d View commit details
    Browse the repository at this point in the history

  16. snorm_norm_rpow

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    9804605 View commit details
    Browse the repository at this point in the history

  17. change the name of a variable

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    b3374d3 View commit details
    Browse the repository at this point in the history

  18. remove a lemma

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    96c9883 View commit details
    Browse the repository at this point in the history

  19. replace pos hypothesis with nonneg

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    e95a0cb View commit details
    Browse the repository at this point in the history

  20. reorder proof

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    a2eb745 View commit details
    Browse the repository at this point in the history

  21. remove unused arguments

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    13bb99a View commit details
    Browse the repository at this point in the history

  22. refactor integral_clm

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    c52b0ce View commit details
    Browse the repository at this point in the history

  23. add is_R_or_C linear maps

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    73a2112 View commit details
    Browse the repository at this point in the history

  24. Merge remote-tracking branch 'origin/master' into l2_space

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    6b828b1 View commit details
    Browse the repository at this point in the history

  25. Merge remote-tracking branch 'origin/more_rpow' into l2_space

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    5a1d00b View commit details
    Browse the repository at this point in the history

  26. Merge remote-tracking branch 'origin/complex_clm' into l2_space

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    80339ac View commit details
    Browse the repository at this point in the history

  27. Merge remote-tracking branch 'origin/ennreal_bit0' into l2_space

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    7802bef View commit details
    Browse the repository at this point in the history

  28. fix merge

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    bd10b76 View commit details
    Browse the repository at this point in the history

  29. fix

    @RemyDegenne
    RemyDegenne committed Mar 10, 2021
    Configuration menu
    Copy the full SHA
    4d773f1 View commit details
    Browse the repository at this point in the history

Commits on Mar 11, 2021

  1. Merge remote-tracking branch 'origin/master' into l2_space

    @RemyDegenne
    RemyDegenne committed Mar 11, 2021
    Configuration menu
    Copy the full SHA
    e7c3683 View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2021

  1. G -> F

    @RemyDegenne
    RemyDegenne committed Mar 13, 2021
    Configuration menu
    Copy the full SHA
    aa46ac8 View commit details
    Browse the repository at this point in the history

Commits on Mar 14, 2021

  1. Merge remote-tracking branch 'origin/master' into more_rpow

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    2229f9f View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/more_rpow' into l2_space

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    ee939b6 View commit details
    Browse the repository at this point in the history

  3. remove duplicate lemma

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    b03ba72 View commit details
    Browse the repository at this point in the history

  4. use inner product notation

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    9637109 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/master' into l2_space

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    2f17d48 View commit details
    Browse the repository at this point in the history

  6. shorten ae_measurable.inner

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    a8bc403 View commit details
    Browse the repository at this point in the history

  7. remove unused variables

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    93444e8 View commit details
    Browse the repository at this point in the history

  8. remove G

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    fb4551f View commit details
    Browse the repository at this point in the history

  9. minor changes

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    a32904c View commit details
    Browse the repository at this point in the history

  10. inner notation

    @RemyDegenne
    RemyDegenne committed Mar 14, 2021
    Configuration menu
    Copy the full SHA
    b83961c View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2021

  1. move lemma about square

    @RemyDegenne
    RemyDegenne committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    78cb1d2 View commit details
    Browse the repository at this point in the history

  2. fix

    @RemyDegenne
    RemyDegenne committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    6067df6 View commit details
    Browse the repository at this point in the history

  3. fix

    @RemyDegenne
    RemyDegenne committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    330e6ed View commit details
    Browse the repository at this point in the history

  4. add file docstring and L2 namespace

    @RemyDegenne
    RemyDegenne committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    752df5e View commit details
    Browse the repository at this point in the history

  5. add docstring to two_mul_le_add_pow_two 

    Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
    @RemyDegenne @hrmacbeth
    RemyDegenne and hrmacbeth committed Mar 15, 2021
    Configuration menu
    Copy the full SHA
    d7fae90 View commit details
    Browse the repository at this point in the history

Commits on Mar 16, 2021

  1. add links to undergrad.yaml

    @RemyDegenne
    RemyDegenne committed Mar 16, 2021
    Configuration menu
    Copy the full SHA
    f6ec4b6 View commit details
    Browse the repository at this point in the history

  2. change a docstring and add L2 notation

    @RemyDegenne
    RemyDegenne committed Mar 16, 2021
    Configuration menu
    Copy the full SHA
    6ba8236 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'l2_space' of github.com:leanprover-community/mathlib in… 

    …to l2_space
    @RemyDegenne
    RemyDegenne committed Mar 16, 2021
    Configuration menu
    Copy the full SHA
    a3df8ed View commit details
    Browse the repository at this point in the history

Commits on Mar 17, 2021

  1. use L2 notation and add name to inner product space instance

    @RemyDegenne
    RemyDegenne committed Mar 17, 2021
    Configuration menu
    Copy the full SHA
    914aa7b View commit details
    Browse the repository at this point in the history

  2. move the definition of the L2 notation

    @RemyDegenne
    RemyDegenne committed Mar 17, 2021
    Configuration menu
    Copy the full SHA
    aa265f8 View commit details
    Browse the repository at this point in the history

  3. localize notations

    @RemyDegenne
    RemyDegenne committed Mar 17, 2021
    Configuration menu
    Copy the full SHA
    2f87cd5 View commit details
    Browse the repository at this point in the history

  4. fix

    @RemyDegenne
    RemyDegenne committed Mar 17, 2021
    Configuration menu
    Copy the full SHA
    cc2efaa View commit details
    Browse the repository at this point in the history