OAI/Analysis/CircleDomains/Topology/RationalQuantileIntervals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed countable family suffices for the four separated quantile arcs.

  1. theorem OAI.CircleDomainRigidity.exists_rational_interval_inside line 14
  2. theorem OAI.CircleDomainRigidity.exists_four_ordered_rational_intervals line 29
  3. theorem OAI.CircleDomainRigidity.exists_four_ordered_rational_intervals_between line 54

    Source documentation

    If the law is supported between two cut points, the four intervals can be chosen strictly inside those cut points.

    theorem exists_four_ordered_rational_intervals_between (μ : Measure ℝ)
    [IsProbabilityMeasure μ] [NullSingletonClass μ] (a b : ℝ)
    (ha : cdf μ a = 0) (hb : cdf μ b = 1) :
    ∃ l u : Fin 4 → ℚ,
      (∀ i, a < (l i : ℝ) ∧ l i < u i ∧ (u i : ℝ) < b ∧
        (1 / 10 : ℝ≥0∞) < μ (Ioo (l i : ℝ) (u i : ℝ))) ∧
      ∀ i j, i < j → u i < l j := by
…