make `cdf` an instance of `Cumulative`

[affeldt-aist]

https://github.com/math-comp/analysis/blob/2f645cfffd5ee1c8abfda6f8deee2110af0c1db7/theories/probability.v#L151-L152

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: https://github.com/math-comp/analysis/blob/6e62b37d02cb8fd357a054a91c160e07671a7d40/theories/topology_theory/order_topology.v#L38-L40

[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. :smile:

[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?

[Yosuke-Ito-345]

@CohenCyril @affeldt-aist @t6s @hoheinzollern @zstone1 @pi8027 I examined the phenomenon in detail. Now I think cumulative_3.txt is the only solution... That is to add

#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : realType) :=
  Order_isNbhs.Build _ R (@real_order_nbhsE R).

in the same manner as realFieldType in num_topology. Is this solution acceptable? (Of course, I don't want to use non-forgetful inheritance.) @zstone1 Your inspection was right. Sorry for not figuring out earlier.

[Yosuke-Ito-345]

FYI @CohenCyril @affeldt-aist @t6s @hoheinzollern @zstone1 @pi8027 The extended real \bar R doesn't seem to equip the OrderNbhs structure, so I'm formalizing

Lemma ereal_order_nbhsE : forall x : (\bar R), nbhs x = filter_from
  (fun i => itv_open_ends i /\ x \in i) (fun i => [set` i]).
HB.instance Definition _ := Order_isNbhs.Build _ (\bar R) ereal_order_nbhsE.

I don't think it causes a problem, but please let me know if you have any concerns.