MeasureTheory/Constructions/AddChar.lean

Stream: mathlib4

[Damiano Testa]

docs#AddChar.instMeasurableSpace and docs#AddChar.instDiscreteMeasurableSpace take only an AddMonoid assumption on A. However, the module docs claims

This file endows `AddChar A M` with the discrete measurable space structure whenever `A` and `M`
are themselves discrete measurable spaces.

and the variables

  [MeasurableSpace A] [DiscreteMeasurableSpace A] [MeasurableSpace M] [DiscreteMeasurableSpace M]

present in the file, do not actually make it into the definition. I suspect that something is off here, right?

I'll ping @Yaël Dillies as author of the file, but I have not investigated who actually introduced this.

[Yaël Dillies]

Indeed that's an accident

[Damiano Testa]

I noticed thanks to the linter that warned me of unused variables and when I saw the file I thought "here is a bug that I will have to fix", but now it seems that this is a bug for you! :smile:

[Damiano Testa]

I am not sure how to proceed, though, since I do not think that include works with the "old" variable inclusion mechanism that instances use.

[Yaël Dillies]

I think they can just be moved to the statements?

[Damiano Testa]

Ok, does this look alright?

namespace AddChar
variable {A M : Type*} [AddMonoid A] [Monoid M] [MeasurableSpace A] [MeasurableSpace M]

instance instMeasurableSpace [DiscreteMeasurableSpace A] [DiscreteMeasurableSpace M] :
    MeasurableSpace (AddChar A M) :=
  ⊤

instance instDiscreteMeasurableSpace [DiscreteMeasurableSpace A] [DiscreteMeasurableSpace M] :
    DiscreteMeasurableSpace (AddChar A M) :=
  ⟨fun _ ↦ trivial⟩

end AddChar

[Damiano Testa]

(I also checked that the linter does not complain about unused variables and hovers show that all variables are now included in the declarations.)

[Damiano Testa]

#18494