import PhysicsLogic.Papers.DurrGoldsteinZanghi1992

open MeasureTheory PhysicsLogic.Papers.DurrGoldsteinZanghi1992
open scoped BigOperators ENNReal
variable {C E T : Type} [MeasurableSpace C] [MeasurableSpace E]

example : ∀ d : TimeAgreementData C E T, d.JointFailureBound ↔
    d.initialLaw {q | ∃ i : Fin d.timeCount,
      let e := d.testsAt (d.timeAt i)
      ∃ p : Fin e.testCount, e.tolerance <
        |(∑ j, e.test p (e.sample j q)) / e.sampleCount -
          ∫ x, e.test p x ∂e.referenceLaw (e.environmentOf q)|} ≤
      ∑ i, ENNReal.ofReal (d.testsAt (d.timeAt i)).totalBudget :=
  TimeAgreementData.joint_failure_bound_iff_explicit_empirical_union

example : ∀ d : TimeAgreementData C E T, d.MostTimesFailureBounds ↔
    ∀ r : ENNReal, r ≠ 0 → r ≠ ⊤ →
      d.initialLaw {q | r ≤
        (∑ i : Fin d.timeCount,
          ({q | let e := d.testsAt (d.timeAt i)
            ∃ p : Fin e.testCount, e.tolerance <
              |(∑ j, e.test p (e.sample j q)) / e.sampleCount -
                ∫ x, e.test p x ∂e.referenceLaw (e.environmentOf q)|}
            : Set C).indicator (fun _ => (1 : ENNReal)) q) / d.timeCount} ≤
        ((∑ i, ENNReal.ofReal (d.testsAt (d.timeAt i)).totalBudget) / d.timeCount) / r :=
  TimeAgreementData.most_times_bound_iff_explicit_empirical_fraction

#print axioms TimeAgreementData.joint_failure_bound_iff_explicit_empirical_union
#print axioms TimeAgreementData.most_times_bound_iff_explicit_empirical_fraction