Code

Probability#516

Code

Merged

affeldt-aist merged 17 commits intomastermath-comp/analysis:masterfrom probabilitymath-comp/analysis:probabilityCopy head branch name to clipboardApr 14, 2023

+538-18

Commits

Commits on Apr 14, 2023

• first take at probability theory

  Show description for 97fe5f5
  

  3 peoplecommitted
  97fe5f5

  Copy full SHA for 97fe5f5

• Lemma probability_fin

  

  hoheinzollern

  authored and

  affeldt-aist

  committed
  b61794d

  Copy full SHA for b61794d

• better definition of discrete random variable

  Show description for 48558d7
  affeldt-aist

  committed
  48558d7

  Copy full SHA for 48558d7

• fixes, cleaning

  affeldt-aist

  committed
  5f07836

  Copy full SHA for 5f07836

• get rid of specialized notations

  affeldt-aist

  committed
  f9cbbc6

  Copy full SHA for f9cbbc6

• get rid of specialized notations (cont'd)

  affeldt-aist

  committed
  8ba1563

  Copy full SHA for 8ba1563

• generalize probability_integrable_cst

  affeldt-aist

  committed
  fbff6dd

  Copy full SHA for fbff6dd

• rm 'E notation, mabs and mexp

  affeldt-aist

  committed
  3cd3a92

  Copy full SHA for 3cd3a92

• wip

  affeldt-aist

  committed
  7b891c7

  Copy full SHA for 7b891c7

• changelog

  affeldt-aist

  committed
  cadde37

  Copy full SHA for cadde37

• fix changelog

  affeldt-aist

  committed
  fbe1c41

  Copy full SHA for fbe1c41

• gen expectation_le

  affeldt-aist

  committed
  ee18e3e

  Copy full SHA for ee18e3e

• generalize le_er_map

  affeldt-aist

  committed
  b4a4490

  Copy full SHA for b4a4490

• tentative def of Lp spaces using quotient

  affeldt-aist

  committed
  972e94a

  Copy full SHA for 972e94a

• Update theories/probability.v

  Show description for 4a26af7
  

  affeldt-aist

  and

  proux01

  committed
  4a26af7

  Copy full SHA for 4a26af7

• use powere_pos, fixes

  affeldt-aist

  committed
  4b0c430

  Copy full SHA for 4b0c430

• rm lspace

  affeldt-aist

  committed
  06adee5

  Copy full SHA for 06adee5