Commits

Branch selector

 master

User selector

RemyDegenne

All time

Commit History

Commits on Feb 23, 2024

• feat: add measurableSet_tendsto_nhds (leanprover-community#10146)

  RemyDegenne

  committedFeb 23, 2024
  f5e69ec

Commits on Feb 22, 2024

• feat: add versions of the monotone convergence theorem for the Bochner integral (leanprover-community#10793)

  RemyDegenne

  committedFeb 22, 2024
  eaba122

• feat: add integral_eq_iff_of_ae_le (leanprover-community#10792)

  RemyDegenne

  committedFeb 22, 2024
  1443e14

• feat: add variants of tendsto_integral_of_L1 (leanprover-community#10790)

  RemyDegenne

  committedFeb 22, 2024
  dc07ce1

• feat: range of enumerateCountable when the default value belongs to the set (leanprover-community#10787)

  RemyDegenne

  committedFeb 22, 2024
  ae0fb61

Commits on Feb 21, 2024

• feat: add tendsto_atBot_atTop_of_antitone (leanprover-community#10794)

  RemyDegenne

  committedFeb 21, 2024
  65d9c6c

• feat: add MeasurableEmbedding.comap_add (leanprover-community#10795)

  RemyDegenne

  committedFeb 21, 2024
  bafc1ac

• feat: add tendsto_nat_ceil_atTop (leanprover-community#10786)

  RemyDegenne

  committedFeb 21, 2024
  807b7b4

• feat: add kernel.(co)map_id (leanprover-community#10801)

  RemyDegenne

  committedFeb 21, 2024
  24c9aaa

• chore: add @[simp] to limsup_const and liminf_const (leanprover-community#10798)

  RemyDegenne

  committedFeb 21, 2024
  7d7cd8c

• feat: MeasurableSpace.generateFrom lemmas (leanprover-community#10797)

  RemyDegenne

  committedFeb 21, 2024
  79d097f

• feat: add snorm_restrict_le (leanprover-community#10788)

  RemyDegenne

  committedFeb 21, 2024
  e6bc0f5

• feat: instances CovariantAddLE and OrderBot for kernel (leanprover-community#10802)

  RemyDegenne

  committedFeb 21, 2024
  88a36ee

Commits on Jan 18, 2024

• feat(MeasureTheory): define contents on semi-rings of sets (leanprover-community#9402)

  RemyDegenne

  committedJan 18, 2024
  6cdea12

• feat(Probability): condKernel and condDistrib applied to singletons of non-zero measure (leanprover-community#9351)

  RemyDegenne

  committedJan 18, 2024
  1bf390a

Commits on Jan 16, 2024

• feat(Probability): simple kernel lemmas (leanprover-community#9350)

  RemyDegenne

  committedJan 16, 2024
  e8248a2

Commits on Dec 31, 2023

• feat(MeasureTheory): log-likelihood ratio of two measures (leanprover-community#9355)

  RemyDegenne

  committedDec 31, 2023
  aa6b836

Commits on Dec 20, 2023

• feat(MeasureTheory): define semi-rings of sets (leanprover-community#8867)

  

  RemyDegenne

  and

  sgouezel

  committedDec 20, 2023
  fdfe843

• feat: projective families of measures and projective limits (leanprover-community#8933)

  RemyDegenne

  committedDec 20, 2023
  905338f

Commits on Dec 18, 2023

• feat: properties of x ↦ - x * log x (leanprover-community#8922)

  

  RemyDegenne

  and

  eric-wieser

  committedDec 18, 2023
  6a04469

Commits on Dec 7, 2023

• feat: exponentially tilted measures (leanprover-community#7676)

  RemyDegenne

  committedDec 7, 2023
  5522fc3

• feat: define the composition-product of a measure and a kernel (leanprover-community#8852)

  RemyDegenne

  committedDec 7, 2023
  cd73b84

Commits on Dec 5, 2023

• feat: pi-systems generating the product sigma algebra (leanprover-community#7566)

  

  RemyDegenne

  and

  YaelDillies

  committedDec 5, 2023
  55a024a

Commits on Nov 30, 2023

• feat(Probability/Independence): add conditional independence (leanprover-community#6098)

  RemyDegenne

  committedNov 30, 2023
  ab3f697

Commits on Nov 21, 2023

• feat(Probability): add simp lemmas for kernels (leanprover-community#8497)

  RemyDegenne

  committedNov 21, 2023
  7d85f2f

Commits on Nov 14, 2023

• feat: generalize some lemmas using withDensity_apply' (leanprover-community#8383)

  

  RemyDegenne

  and

  sgouezel

  committedNov 14, 2023
  21b5939

Commits on Nov 12, 2023

• feat(MeasureTheory): remove an AbsolutelyContinuous hypothesis from inv_rnDeriv (leanprover-community#8351)

  RemyDegenne

  committedNov 12, 2023
  daf40d2

• feat(MeasureTheory): integrals of rnDeriv without absolute continuity (leanprover-community#8343)

  RemyDegenne

  committedNov 12, 2023
  708c4de

Commits on Nov 8, 2023

• chore: split MeasureTheory.Decomposition.Lebesgue (leanprover-community#8272)

  RemyDegenne

  committedNov 8, 2023
  fe7e9d0

• feat: SigmaFinite instances for Measure.withDensity (leanprover-community#8271)

  RemyDegenne

  committedNov 8, 2023
  0821e8f

Commits on Nov 7, 2023

• feat: add Integrable.piecewise (leanprover-community#8080)

  RemyDegenne

  committedNov 7, 2023
  18d2099

Commits on Nov 2, 2023

• feat: properties of rnDeriv (leanprover-community#7675)

  

  RemyDegenne

  and

  digama0

  committedNov 2, 2023
  9fa322a

Commits on Nov 1, 2023

• feat: Inf variants of ciSup_mul and related lemmas (leanprover-community#8078)

  RemyDegenne

  committedNov 1, 2023
  aedc01b

Commits on Oct 30, 2023

• feat(MeasureTheory): μ.singularPart (r • ν) = μ.singularPart ν (leanprover-community#8040)

  RemyDegenne

  committedOct 30, 2023
  333277c

• feat: if X is Gaussian, then X+y and c*X are Gaussian (leanprover-community#7674)

  

  RemyDegenne

  and

  digama0

  committedOct 30, 2023
  185dddf

Pagination

PreviousNext