!4#4557 Probability.Indepence.Basic

Stream: mathlib4

[Xavier Roblot]

The file probability.independence.basic has several definitions or lemmas containing Indep, eg. docs#probability_theory.Indep or docs#probability_theory.Indep.Indep_sets. To deal with those, Mathport has been adding Cat at the end of the names but that is obviously wrong. So what would be the right naming scheme here?

[Heather Macbeth]

I think the naming scheme for the various flavours of Union should work.

[Rémy Degenne]

To come up with the names Indep/indep, I copied Union/union for sets. So whatever is used for those.

[Xavier Roblot]

So that would give iIndep to replace Indep then

[Xavier Roblot]

In the same file, the following lemma

@[symm]
theorem IndepFun.symm {mβ : MeasurableSpace β} {f g : Ω → β} (hfg : IndepFun f g μ) :
    IndepFun g f μ := hfg.symm

gives the error

fail to show termination for
  ProbabilityTheory.IndepFun.symm
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'ProbabilityTheory.IndepFun.symm' does not take any (non-fixed) arguments

In Mathlib3, it was stated as

@[symm] lemma indep_fun.symm {mβ : measurable_space β} {f g : Ω → β} (hfg : indep_fun f g μ) :
  indep_fun g f μ :=
hfg.symm

so essentially the same...

[Moritz Doll]

you want to add nonrec in front of you theorem

[Moritz Doll]

Lean 4 tries to apply IndepFun.symm for hfg.symm, whereas Lean 3 used something else