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(Probability/Kernel): disintegration of finite kernels #10603

Closed
wants to merge 150 commits into from
Closed

[Merged by Bors] - feat(Probability/Kernel): disintegration of finite kernels #10603

wants to merge 150 commits into from

Commits on Feb 1, 2024

  1. partial work towards kernel disintegration

    @RemyDegenne
    RemyDegenne committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    d5f79f0 View commit details
    Browse the repository at this point in the history

  2. refactor defaultRatCDF

    @RemyDegenne
    RemyDegenne committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    a9b011c View commit details
    Browse the repository at this point in the history

  3. remove comment

    @RemyDegenne
    RemyDegenne committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    8d1da47 View commit details
    Browse the repository at this point in the history

  4. minor

    @RemyDegenne
    RemyDegenne committed Feb 1, 2024
    Configuration menu
    Copy the full SHA
    099b859 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2024

  1. more work

    @RemyDegenne
    RemyDegenne committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    bf37c05 View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2024

  1. almost done

    @RemyDegenne
    RemyDegenne committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    2c9e449 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    d9d8f9f View commit details
    Browse the repository at this point in the history

  3. move files

    @RemyDegenne
    RemyDegenne committed Feb 12, 2024
    Configuration menu
    Copy the full SHA
    d28bd4c View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2024

  1. save

    @RemyDegenne
    RemyDegenne committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    48afecb View commit details
    Browse the repository at this point in the history

  2. add IsKernelCDF

    @RemyDegenne
    RemyDegenne committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    71e4115 View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2024

  1. rename todo2 lemmas

    @RemyDegenne
    RemyDegenne committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    242d5f5 View commit details
    Browse the repository at this point in the history

  2. reorganize. WIP

    @RemyDegenne
    RemyDegenne committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    6ea94c4 View commit details
    Browse the repository at this point in the history

  3. split files

    @RemyDegenne
    RemyDegenne committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    8012c6d View commit details
    Browse the repository at this point in the history

  4. generalize to finite kernel

    @RemyDegenne
    RemyDegenne committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    c7492e9 View commit details
    Browse the repository at this point in the history

  5. main proof done

    @RemyDegenne
    RemyDegenne committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    575a4c9 View commit details
    Browse the repository at this point in the history

Commits on Feb 15, 2024

  1. uniqueness of kernel.condexpKernel

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    8edfabd View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    f708964 View commit details
    Browse the repository at this point in the history

  3. add Integral file

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    85f4952 View commit details
    Browse the repository at this point in the history

  4. move results, fix

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    47b1d65 View commit details
    Browse the repository at this point in the history

  5. docstring for Integral.lean

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    76961e9 View commit details
    Browse the repository at this point in the history

  6. move/extract lemmas

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    9d97cb1 View commit details
    Browse the repository at this point in the history

  7. various minor

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    cfde47b View commit details
    Browse the repository at this point in the history

  8. rename files

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    be152bb View commit details
    Browse the repository at this point in the history

  9. fix space

    @RemyDegenne
    RemyDegenne committed Feb 15, 2024
    Configuration menu
    Copy the full SHA
    7544dac View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2024

  1. docstrings in MeasurableStieltjes

    @RemyDegenne
    RemyDegenne committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    be68022 View commit details
    Browse the repository at this point in the history

  2. add docstring

    @RemyDegenne
    RemyDegenne committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    7f42f9f View commit details
    Browse the repository at this point in the history

  3. Mathlib.lean

    @RemyDegenne
    RemyDegenne committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    75e3389 View commit details
    Browse the repository at this point in the history

  4. fix

    @RemyDegenne
    RemyDegenne committed Feb 16, 2024
    Configuration menu
    Copy the full SHA
    2de05e6 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2024

  1. change KernelCDFBorel to prepare for kernel Radon-Nikodym

    @RemyDegenne
    RemyDegenne committed Feb 17, 2024
    Configuration menu
    Copy the full SHA
    ef5d237 View commit details
    Browse the repository at this point in the history

  2. rename

    @RemyDegenne
    RemyDegenne committed Feb 17, 2024
    Configuration menu
    Copy the full SHA
    e993e5d View commit details
    Browse the repository at this point in the history

  3. reorder arguments

    @RemyDegenne
    RemyDegenne committed Feb 17, 2024
    Configuration menu
    Copy the full SHA
    b9d443b View commit details
    Browse the repository at this point in the history

Commits on Feb 18, 2024

  1. split file

    @RemyDegenne
    RemyDegenne committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    3460efd View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    4fada6e View commit details
    Browse the repository at this point in the history

  3. fix

    @RemyDegenne
    RemyDegenne committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    3bb8792 View commit details
    Browse the repository at this point in the history

  4. delete again

    @RemyDegenne
    RemyDegenne committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    237699e View commit details
    Browse the repository at this point in the history

  5. Mathlib.lean

    @RemyDegenne
    RemyDegenne committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    ac52950 View commit details
    Browse the repository at this point in the history

  6. fix name

    @RemyDegenne
    RemyDegenne committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    3a77c06 View commit details
    Browse the repository at this point in the history

  7. rename

    @RemyDegenne
    RemyDegenne committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    3f9519b View commit details
    Browse the repository at this point in the history

Commits on Feb 19, 2024

  1. add RadonNikodym

    @RemyDegenne
    RemyDegenne committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    e6145fd View commit details
    Browse the repository at this point in the history

  2. Mathlib.lean

    @RemyDegenne
    RemyDegenne committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    746ef13 View commit details
    Browse the repository at this point in the history

  3. move lemmas

    @RemyDegenne
    RemyDegenne committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    857e3a2 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Probability/Kernel/Disintegration/RadonNikodym.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @RemyDegenne @github-actions
    RemyDegenne and github-actions[bot] committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    29ecce1 View commit details
    Browse the repository at this point in the history

  5. move lemmas

    @RemyDegenne
    RemyDegenne committed Feb 19, 2024
    Configuration menu
    Copy the full SHA
    4ec8637 View commit details
    Browse the repository at this point in the history

Commits on Feb 20, 2024

  1. use CountablyGenerated

    @RemyDegenne
    RemyDegenne committed Feb 20, 2024
    Configuration menu
    Copy the full SHA
    6cc7107 View commit details
    Browse the repository at this point in the history

Commits on Feb 21, 2024

  1. renames and other stuff

    @RemyDegenne
    RemyDegenne committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    774b862 View commit details
    Browse the repository at this point in the history

  2. feat: lemmas about kernel.withDensity

    @RemyDegenne
    RemyDegenne committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    5fb37f9 View commit details
    Browse the repository at this point in the history

  3. fix

    @RemyDegenne
    RemyDegenne committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    45c91cd View commit details
    Browse the repository at this point in the history

  4. updated docstring of Density

    @RemyDegenne
    RemyDegenne committed Feb 21, 2024
    Configuration menu
    Copy the full SHA
    301846d View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2024

  1. add withDensity_add_right

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    d7a7608 View commit details
    Browse the repository at this point in the history

  2. split partitioned

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    54e85f3 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    2ae0930 View commit details
    Browse the repository at this point in the history

  4. fix

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    0d49ff1 View commit details
    Browse the repository at this point in the history

  5. fix

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    bc9ebac View commit details
    Browse the repository at this point in the history

  6. split file

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    4ecd880 View commit details
    Browse the repository at this point in the history

  7. docstring

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    6342f08 View commit details
    Browse the repository at this point in the history

  8. fix

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    6cdfdb4 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 22, 2024
    Configuration menu
    Copy the full SHA
    77d91ce View commit details
    Browse the repository at this point in the history

Commits on Feb 23, 2024

  1. measurability of absolutelyContinuous and mutuallySingular

    @RemyDegenne
    RemyDegenne committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    570d243 View commit details
    Browse the repository at this point in the history

  2. rename

    @RemyDegenne
    RemyDegenne committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    90d8e8b View commit details
    Browse the repository at this point in the history

  3. polish Density.lean

    @RemyDegenne
    RemyDegenne committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    64ed76a View commit details
    Browse the repository at this point in the history

  4. docstrings

    @RemyDegenne
    RemyDegenne committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    534fa29 View commit details
    Browse the repository at this point in the history

  5. typo

    @RemyDegenne
    RemyDegenne committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    2aa1051 View commit details
    Browse the repository at this point in the history

  6. more CountablyGenerated

    @RemyDegenne
    RemyDegenne committed Feb 23, 2024
    Configuration menu
    Copy the full SHA
    777f745 View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2024

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

    @RemyDegenne
    RemyDegenne committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    b0a8c0e View commit details
    Browse the repository at this point in the history

  2. remove aux lemma

    @RemyDegenne
    RemyDegenne committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    02fa789 View commit details
    Browse the repository at this point in the history

  3. split CountablyGenerated file about filtration

    @RemyDegenne
    RemyDegenne committed Feb 24, 2024
    Configuration menu
    Copy the full SHA
    9304920 View commit details
    Browse the repository at this point in the history

Commits on Feb 25, 2024

  1. minor

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    659f8eb View commit details
    Browse the repository at this point in the history

  2. docstring

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    4f47e8d View commit details
    Browse the repository at this point in the history

  3. feat: isCoboundedUnder_le lemmas

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    0f501bc View commit details
    Browse the repository at this point in the history

  4. feat: countable filtration in a countably generated measurable space

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    f3e7ed6 View commit details
    Browse the repository at this point in the history

  5. fix

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    c88f084 View commit details
    Browse the repository at this point in the history

  6. fix

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    2b81b61 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/RD_countablyGenerated' into RD_d… 

    …isintegration
    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    ec9ed75 View commit details
    Browse the repository at this point in the history

  8. fix imports

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    85b299b View commit details
    Browse the repository at this point in the history

  9. fix imports

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    000bd10 View commit details
    Browse the repository at this point in the history

  10. feat: density of a finite kernel wrt another kernel

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    02bfb16 View commit details
    Browse the repository at this point in the history

  11. Merge remote-tracking branch 'origin/RD_cobounded' into RD_density

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    619f397 View commit details
    Browse the repository at this point in the history

  12. docstrings in RN

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    0d8afaf View commit details
    Browse the repository at this point in the history

  13. add RN for kernels

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    e290aed View commit details
    Browse the repository at this point in the history

  14. Merge remote-tracking branch 'origin/RD_withDensity' into RD_kernelRN

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    fd76d2c View commit details
    Browse the repository at this point in the history

  15. fix

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    0b0b32b View commit details
    Browse the repository at this point in the history

  16. Merge remote-tracking branch 'origin/RD_kernelRN' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    cdef823 View commit details
    Browse the repository at this point in the history

  17. delete duplicate

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    715bd03 View commit details
    Browse the repository at this point in the history

  18. clean MeasurableStieltjes

    @RemyDegenne
    RemyDegenne committed Feb 25, 2024
    Configuration menu
    Copy the full SHA
    cb90c8d View commit details
    Browse the repository at this point in the history

Commits on Feb 26, 2024

  1. minor

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    768c1b9 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    df6e0cb View commit details
    Browse the repository at this point in the history

  3. start docstring for CDFKernel

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    ded4b18 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    1c7f426 View commit details
    Browse the repository at this point in the history

  5. fix merge

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    18213af View commit details
    Browse the repository at this point in the history

  6. rename files

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    b05613e View commit details
    Browse the repository at this point in the history

  7. change variable name

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    7870eb8 View commit details
    Browse the repository at this point in the history

  8. docstrings

    @RemyDegenne
    RemyDegenne committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    e2330f2 View commit details
    Browse the repository at this point in the history

Commits on Feb 27, 2024

  1. file name, docstring

    @RemyDegenne
    RemyDegenne committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    d68617d View commit details
    Browse the repository at this point in the history

  2. mostly variable names

    @RemyDegenne
    RemyDegenne committed Feb 27, 2024
    Configuration menu
    Copy the full SHA
    a6a0f91 View commit details
    Browse the repository at this point in the history

Commits on Mar 5, 2024

  1. more work

    @RemyDegenne
    RemyDegenne committed Mar 5, 2024
    Configuration menu
    Copy the full SHA
    6ae4932 View commit details
    Browse the repository at this point in the history

Commits on Mar 6, 2024

  1. refactor

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

  2. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    27fb33e View commit details
    Browse the repository at this point in the history

  3. fix

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

  4. fix

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

  5. delete a file

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

  6. Mathlib.lean

    @RemyDegenne
    RemyDegenne committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    668182e View commit details
    Browse the repository at this point in the history

  7. docstrings

    @RemyDegenne
    RemyDegenne committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    829495e View commit details
    Browse the repository at this point in the history

  8. delete AuxLemmas.lean

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

  9. variables

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

Commits on Mar 10, 2024

  1. more about RN

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

  2. Merge remote-tracking branch 'origin/master' into RD_disintegration

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

  3. remove duplicates

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

Commits on Mar 13, 2024

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

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

  2. remove duplicate file

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

  3. fix

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

  4. fix Mathlib.lean

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

  5. golf

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

  6. docstring

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

  7. line length

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

  8. Merge remote-tracking branch 'origin/RD_density' into RD_kernelRN

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

  9. Merge remote-tracking branch 'origin/RD_kernelRN' into RD_disintegration

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

  10. remove duplicates

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

  11. refactor, with todo names

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

Commits on Mar 20, 2024

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

    @RemyDegenne
    RemyDegenne committed Mar 20, 2024
    Configuration menu
    Copy the full SHA
    7f5adfd View commit details
    Browse the repository at this point in the history

  2. minor changes in CondCdf

    @RemyDegenne
    RemyDegenne committed Mar 20, 2024
    Configuration menu
    Copy the full SHA
    297ade4 View commit details
    Browse the repository at this point in the history

Commits on Mar 27, 2024

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

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

  2. fix merge

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

  3. remove duplicate

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

  4. fix

    @RemyDegenne
    RemyDegenne committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    54dd5ee View commit details
    Browse the repository at this point in the history

Commits on Mar 29, 2024

  1. remove unrelated material

    @RemyDegenne
    RemyDegenne committed Mar 29, 2024
    Configuration menu
    Copy the full SHA
    99f0bc0 View commit details
    Browse the repository at this point in the history

  2. remove import

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

  3. rename embeddingReal

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

  4. make condKernel irreducible

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

  5. don't use Omega'

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

  6. move CountableOrCountablyGenerated

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

  7. undo changes to condCdf

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

Commits on Mar 31, 2024

  1. add docstrings to Basic

    @RemyDegenne
    RemyDegenne committed Mar 31, 2024
    Configuration menu
    Copy the full SHA
    a089953 View commit details
    Browse the repository at this point in the history

  2. add docstrings in Unique.lean

    @RemyDegenne
    RemyDegenne committed Mar 31, 2024
    Configuration menu
    Copy the full SHA
    00b0862 View commit details
    Browse the repository at this point in the history

  3. fix

    @RemyDegenne
    RemyDegenne committed Mar 31, 2024
    Configuration menu
    Copy the full SHA
    f5704dc View commit details
    Browse the repository at this point in the history

Commits on Apr 1, 2024

  1. golf Unique

    @RemyDegenne
    RemyDegenne committed Apr 1, 2024
    Configuration menu
    Copy the full SHA
    3ddfbd8 View commit details
    Browse the repository at this point in the history

  2. lint

    @RemyDegenne
    RemyDegenne committed Apr 1, 2024
    Configuration menu
    Copy the full SHA
    b556324 View commit details
    Browse the repository at this point in the history

Commits on Apr 3, 2024

  1. remove assumption to see what breaks

    @sgouezel
    sgouezel committed Apr 3, 2024
    Configuration menu
    Copy the full SHA
    c361742 View commit details
    Browse the repository at this point in the history

Commits on Apr 5, 2024

  1. measurable atoms

    @sgouezel
    sgouezel committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    2e9b90b View commit details
    Browse the repository at this point in the history

  2. start fixing

    @sgouezel
    sgouezel committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    9325b62 View commit details
    Browse the repository at this point in the history

  3. move to better place, lint, cleanup

    @sgouezel
    sgouezel committed Apr 5, 2024
    Configuration menu
    Copy the full SHA
    0c3e29e View commit details
    Browse the repository at this point in the history

Commits on Apr 6, 2024

  1. fix docstring

    @RemyDegenne
    RemyDegenne committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    486309d View commit details
    Browse the repository at this point in the history

Commits on Apr 7, 2024

  1. refactor real to Borel

    @RemyDegenne
    RemyDegenne committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    cb76215 View commit details
    Browse the repository at this point in the history

  2. remove unused import

    @RemyDegenne
    RemyDegenne committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    a28997d View commit details
    Browse the repository at this point in the history

Commits on Apr 12, 2024

  1. fix merge conflict

    @RemyDegenne
    RemyDegenne committed Apr 12, 2024
    Configuration menu
    Copy the full SHA
    950ddf7 View commit details
    Browse the repository at this point in the history

Commits on Apr 16, 2024

  1. remove some completeness assumptions

    @sgouezel
    sgouezel committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    427687c View commit details
    Browse the repository at this point in the history

  2. lint

    @sgouezel
    sgouezel committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    94bf67e View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into RD_disintegration

    @RemyDegenne
    RemyDegenne committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    1ab7657 View commit details
    Browse the repository at this point in the history

  4. Apply suggestions from code review 

    Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @RemyDegenne @sgouezel
    RemyDegenne and sgouezel committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    51952fc View commit details
    Browse the repository at this point in the history

  5. create Real section at the top of Disintegration/Basic

    @RemyDegenne
    RemyDegenne committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    4c40319 View commit details
    Browse the repository at this point in the history

  6. irreducible_def

    @RemyDegenne
    RemyDegenne committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    0081cac View commit details
    Browse the repository at this point in the history