make `cdf` an instance of `Cumulative`

[affeldt-aist]

analysis/theories/probability.v

Lines 151 to 152 in 2f645cf

	Definition cdf d (T : measurableType d) (R : realType) (P : probability T R)
	(X : {RV P >-> R}) (r : R) := distribution P X `]-oo, r].

cdf should be made an instance of Cumulative (from lebesgue_stieltjes_measure.v),
however functions in Cumulative have codomain R whereas cdf expects codomain `\bar R.
It should be generalized to topological order space.
Introduce of related structures such as cadlag can come later.

see the minutes of the 2025-04-11 meeting

[Yosuke-Ito-345]

A possible plan would be as follows.

1. Introduce an ordered filtered (topological) type O.
2. Change the underlying type of Cumulative from R : numFieldType to O.
3. Make cdf an instance of Cumulative, e.g.

HB.instance Definition _ := isCumulative.Build (\bar R) (cdf X) cdf_nondecreasing cdf_right_continuous.

We would leave the following code in lebesgue_stieltjes_measure.v as it is.

HB.instance Definition _ := isCumulative.Build R idfun id_nd id_rc.

Are we on the same page?

[Yosuke-Ito-345]

@CohenCyril @affeldt-aist @t6s @hoheinzollern @zstone1
Any thoughts on this plan? :-)

[CohenCyril]

@Yosuke-Ito-345 it does sound good! Thanks for pinging me I had not seen your reply.

[CohenCyril]

Note that step 1. is already completed:

analysis/theories/topology_theory/order_topology.v

Lines 38 to 40 in 6e62b37

	#[short(type="orderTopologicalType")]
	HB.structure Definition OrderTopological d :=
	{ T of Topological T & Order.Total d T & Order_isNbhs d T }.

[Yosuke-Ito-345]

@CohenCyril
Oops, I missed the orderTopologicalType. That would be so helpful.
I'll start from step 2. Thank you very much for the reply. 😄

[Yosuke-Ito-345]

@CohenCyril @affeldt-aist @t6s @hoheinzollern @zstone1
Sorry for the repeated questions, but I am struggling with the type inference.
I am changing the codomain of isCumulative to orderTopologicalType.
In the proof of Let id_rc : right_continuous (@idfun R)., the error occurs when I apply right_continuousW (cf. cumulative_1.txt).
However, if I change the type of R from realType to realFieldType, then the same proof of Let id_rc succeeds (cf. cumulative_2.txt).
My understanding is that realType equips realFieldType by Hierarchy Builder. If that is right, the two proofs should be equally successful.
What do I misunderstand?
cumulative_1.txt
cumulative_2.txt

[t6s]

(I have no idea for the original question, but)
Why do you want to specialize the instance to realType?
realFieldType seems to suffice.

[zstone1]

On one hand, yes you might as well enjoy the improved generality of realFieldType. As to why it doesn't work, non-forgetful inheritance is easy to blame (although I admit I can't be sure it is actually the cause of your type-checking failure). In particular, there is a lot of non-forgetful inheritance around realField and friends. See num_topology and normed_module and look for #[export, non_forgetful_inheritance] annotation. Explicitly using R^o sometimes fixes this issue, but creates downstream annoyances. So I wouldn't recommend it unless it's necessary.

[Yosuke-Ito-345]

Thank you both for the replies.
@t6s It is because the original code is realType. In addition, if I replace all the realTypes to realFieldTypes, then another part breaks. Currently I am not sure how to fix it.
@zstone1 I didn't know non_forgetful_inheritance. Now I'm going to work, I will look it up on the reference later. Thank you again for the pointer.

[Yosuke-Ito-345]

@CohenCyril @affeldt-aist @t6s @hoheinzollern @zstone1 @pi8027
Sorry for the repeated questions. I have been unable to find an answer to this question.
I studied the non-forgetful inheritance but it is not likely the clue. Furthermore, I got another question...
Since the proof of Let id_rc in cumulative_2.txt succeeds, I think the realFieldType R is considered as an orderTopologicalType.
However, if I do HB.about realFieldType. in cumulative_2.txt, I get

HB: Num.RealField inherits from:
    - eqtype.Equality
    - choice.Choice
    - Order.POrder
    - GRing.Nmodule
    - GRing.Zmodule
    - Num.SemiNormedZmodule
    - GRing.PzSemiRing
    - GRing.PzRing
    - Num.POrderedZmodule
    - GRing.NzSemiRing
    - GRing.NzRing
    - GRing.UnitRing
    - Num.NormedZmodule
    - Order.MeetSemilattice
    - Order.JoinSemilattice
    - Order.Lattice
    - Order.DistrLattice
    - Order.Total
    - GRing.ComPzSemiRing
    - GRing.ComPzRing
    - GRing.ComNzSemiRing
    - GRing.ComNzRing
    - GRing.ComUnitRing
    - GRing.IntegralDomain
    - Num.NumDomain
    - Num.RealDomain
    - GRing.Field
    - Num.NumField

It does not include orderTopologicalType. Why is such unification possible?