Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(probability/integration): Bochner integral of the product of independent functions #13140

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(probability/integration): Bochner integral of the product of independent functions #13140

wants to merge 5 commits into from

Commits on Apr 2, 2022

  1. feat(probability/integration): Bochner integral of the product of ind… 

    …ependent functions
    @vbeffara
    vbeffara committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    2e7b7a7 View commit details
    Browse the repository at this point in the history

  2. No need for probability notation

    @vbeffara
    vbeffara committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    3270632 View commit details
    Browse the repository at this point in the history

  3. Extend indep_fun.integrable_mul a little

    @vbeffara
    vbeffara committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    177f528 View commit details
    Browse the repository at this point in the history

Commits on Apr 6, 2022

  1. Following Remy's suggestions

    @vbeffara
    vbeffara committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    3bbb824 View commit details
    Browse the repository at this point in the history

  2. Massage the code a bit more

    @vbeffara
    vbeffara committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    6ff154e View commit details
    Browse the repository at this point in the history