Theorem ProbabilityTheory.kernel.tendsto_density_atTop_ae_of_antitone

Modification history

2024-07-23 07:55

Mathlib/Probability/Kernel/Disintegration/Density.lean

refactor(Probability): Make kernels a type (#15021) …

Deleted ProbabilityTheory.kernel.tendsto_density_atTop_ae_of_antitone View on Github →

2024-03-20 15:45

Mathlib/Probability/Kernel/Disintegration/Density.lean

feat: density of a finite kernel wrt another kernel (#10948) …

Added ProbabilityTheory.kernel.tendsto_density_atTop_ae_of_antitone View on Github →