feat: variance of the binomial distribution

[EtienneC30]

---

• depends on: feat: a sum of independent Bernoulli random variables is a binomial random variable #37794
• depends on: feat: lemmas about MemLp #43001

[github-actions]

PR summary 60568b4236

Import changes exceeding 2%

%	File
+18.26%	Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+19.01%	Mathlib.Probability.Distributions.Bernoulli

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Probability.Distributions.Bernoulli	2335	2779	+444 (+19.01%)
Mathlib.MeasureTheory.Function.LpSeminorm.Basic	1939	2293	+354 (+18.26%)
Mathlib.Probability.Distributions.Binomial	2856	2859	+3 (+0.11%)
Mathlib.Probability.Distributions.SetBernoulli	2854	2855	+1 (+0.04%)

Import changes for all files

Files	Import difference
Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs Mathlib.Probability.Distributions.SetBernoulli	1
3 files Mathlib.Probability.Distributions.Binomial Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.ProbabilityMassFunction.Binomial	3
Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions	280
5 files Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSpace.Basic Mathlib.MeasureTheory.Function.LpSpace.Complete Mathlib.MeasureTheory.Function.LpSpace.Indicator	282
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality	318
Mathlib.Probability.Distributions.Uniform	346
8 files Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.MeasureTheory.Function.LpSeminorm.Count Mathlib.MeasureTheory.Function.LpSeminorm.Indicator Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity Mathlib.MeasureTheory.Function.LpSeminorm.Prod Mathlib.MeasureTheory.Function.LpSeminorm.SMul Mathlib.MeasureTheory.Function.LpSeminorm.Trim	354
Mathlib.Probability.ProbabilityMassFunction.Integrals	429
Mathlib.Probability.Distributions.Bernoulli Mathlib.Probability.ProbabilityMassFunction.Constructions	444

---

Declarations diff (regex)

+ HasLaw.hasLaw_indicator_infinitePi_ite_of_setBernoulli
+ HasLaw.hasLaw_indicator_one_infinitePi_ite_of_setBernoulli
+ HasLaw.indicator_of_setBernoulli_of_mem
+ HasLaw.indicator_of_setBernoulli_of_notMem
+ HasLaw.indicator_one_of_setBernoulli_of_mem
+ HasLaw.integrable
+ HasLaw.integrable_bernoulliMeasure
+ HasLaw.integrable_comp
+ HasLaw.integrable_comp_bernoulliMeasure
+ HasLaw.memLp
+ HasLaw.memLp_bernoulliMeasure
+ HasLaw.memLp_comp
+ HasLaw.memLp_comp_bernoulliMeasure
+ LpAddConst_ne_zero
+ MemLp.add_measure
+ MemLp.smul_measure_nnreal
+ dirac_real_apply
+ dirac_real_apply_of_mem
+ eLpNormEssSup_add_measure
+ eLpNormEssSup_dirac
+ eq_bernoulliMeasure
+ essInf_dirac
+ essSup_dirac
+ hasLaw_indicator_bernoulliMeasure
+ hasLaw_indicator_one_bernoulliMeasure
+ hasLaw_map
+ iIndepFun.hasLaw_finsetSum_binomial
+ iIndepFun.hasLaw_finsetSum_map_cast_binomial
+ iIndepFun.hasLaw_sum_binomial
+ iIndepFun.hasLaw_sum_map_cast_binomial
+ integral_id_bernoulliMeasure
+ integral_id_binomial
+ liminf_pure
+ limsInf_pure
+ limsSup_pure
+ limsup_pure
+ measurePreserving_ncard_setBernoulli_binomial_ncard
+ memLp_add_measure
+ memLp_bernoulliMeasure
+ memLp_dirac
+ setBernoulli_mem_of_mem
+ setBernoulli_mem_of_notMem
+ setBernoulli_real_mem_of_mem
+ setBernoulli_real_mem_of_notMem
+ variance_id_bernoulliMeasure
+ variance_id_binomial
+ variance_of_hasLaw_binomial

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 60568b4).

• +49 new declarations
• −0 removed declarations

+ENNReal.LpAddConst_ne_zero
+Filter.liminf_pure
+Filter.limsInf_pure
+Filter.limsSup_pure
+Filter.limsup_pure
+MeasureTheory.Measure.dirac_real_apply
+MeasureTheory.Measure.dirac_real_apply_of_mem
+MeasureTheory.MemLp.add_measure
+MeasureTheory.MemLp.smul_measure_nnreal
+MeasureTheory.eLpNormEssSup_add_measure
+MeasureTheory.eLpNormEssSup_dirac
+MeasureTheory.memLp_add_measure
+MeasureTheory.memLp_dirac
+ProbabilityTheory.HasLaw.hasLaw_indicator_infinitePi_ite_of_setBernoulli
+ProbabilityTheory.HasLaw.hasLaw_indicator_one_infinitePi_ite_of_setBernoulli
+ProbabilityTheory.HasLaw.indicator_of_setBernoulli_of_mem
+ProbabilityTheory.HasLaw.indicator_of_setBernoulli_of_notMem
+ProbabilityTheory.HasLaw.indicator_one_of_setBernoulli_of_mem
+ProbabilityTheory.HasLaw.integrable
+ProbabilityTheory.HasLaw.integrable_bernoulliMeasure
+ProbabilityTheory.HasLaw.integrable_comp
+ProbabilityTheory.HasLaw.integrable_comp_bernoulliMeasure
+ProbabilityTheory.HasLaw.integrable_fun_comp
+ProbabilityTheory.HasLaw.memLp
+ProbabilityTheory.HasLaw.memLp_bernoulliMeasure
+ProbabilityTheory.HasLaw.memLp_comp
+ProbabilityTheory.HasLaw.memLp_comp_bernoulliMeasure
+ProbabilityTheory.HasLaw.memLp_fun_comp
+ProbabilityTheory.eq_bernoulliMeasure
+ProbabilityTheory.hasLaw_indicator_bernoulliMeasure
+ProbabilityTheory.hasLaw_indicator_one_bernoulliMeasure
+ProbabilityTheory.hasLaw_map
+ProbabilityTheory.iIndepFun.hasLaw_finsetSum_binomial
+ProbabilityTheory.iIndepFun.hasLaw_finsetSum_map_cast_binomial
+ProbabilityTheory.iIndepFun.hasLaw_sum_binomial
+ProbabilityTheory.iIndepFun.hasLaw_sum_map_cast_binomial
+ProbabilityTheory.integral_id_bernoulliMeasure
+ProbabilityTheory.integral_id_binomial
+ProbabilityTheory.measurePreserving_ncard_setBernoulli_binomial_ncard
+ProbabilityTheory.memLp_bernoulliMeasure
+ProbabilityTheory.setBernoulli_mem_of_mem
+ProbabilityTheory.setBernoulli_mem_of_notMem
+ProbabilityTheory.setBernoulli_real_mem_of_mem
+ProbabilityTheory.setBernoulli_real_mem_of_notMem
+ProbabilityTheory.variance_id_bernoulliMeasure
+ProbabilityTheory.variance_id_binomial
+ProbabilityTheory.variance_of_hasLaw_binomial
+essInf_dirac
+essSup_dirac

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 60568b4236
Reference commit 9b397f578e

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: a sum of independent Bernoulli random variables is a binomial random variable #37794
• feat: lemmas about MemLp #43001
  By Dependent Issues (🤖). Happy coding!

[EtienneC30]

splice-bot

[mathlib-splicebot]

Split PR created

Split off the changes to Mathlib/Probability/HasLaw.lean in #43002.