OAI/Combinatorics/SharpThreshold/QuantileAnalysis.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.quantile_attainment_of_strictMonoOn line 11

   Source documentation

   A continuous strictly increasing distribution on the unit interval attains its infimum-defined quantiles at unique interior points.

   theorem quantile_attainment_of_strictMonoOn
       {μ : ℝ → ℝ} (hcont : ContinuousOn μ (Set.Icc 0 1))
       (hmono : StrictMonoOn μ (Set.Icc 0 1))
       (hzero : μ 0 = 0) (hone : μ 1 = 1)
       {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
       let q := sInf {p : ℝ | p ∈ Set.Icc (0 : ℝ) 1 ∧ a ≤ μ p}
   …

2. theorem OAI.Problem313.strictMonoOn_unit_of_hasDerivAt_pos line 52

   Source documentation

   Positive derivatives in the interior imply the strict monotonicity required by the quantile attainment theorem; endpoints only require continuity.

   theorem strictMonoOn_unit_of_hasDerivAt_pos
       {μ D : ℝ → ℝ} (hcont : ContinuousOn μ (Set.Icc 0 1))
       (hderiv : ∀ p ∈ Set.Ioo (0 : ℝ) 1, HasDerivAt μ (D p) p)
       (hpos : ∀ p ∈ Set.Ioo (0 : ℝ) 1, 0 < D p) :
       StrictMonoOn μ (Set.Icc (0 : ℝ) 1) := by
   …

3. theorem OAI.Problem313.quantile_attainment_of_hasDerivAt_pos line 64

   Source documentation

   The quantile width estimate in derivative form.

   theorem quantile_attainment_of_hasDerivAt_pos
       {μ D : ℝ → ℝ} (hcont : ContinuousOn μ (Set.Icc 0 1))
       (hderiv : ∀ p ∈ Set.Ioo (0 : ℝ) 1, HasDerivAt μ (D p) p)
       (hpos : ∀ p ∈ Set.Ioo (0 : ℝ) 1, 0 < D p)
       (hzero : μ 0 = 0) (hone : μ 1 = 1)
       {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) :
       let q := sInf {p : ℝ | p ∈ Set.Icc (0 : ℝ) 1 ∧ a ≤ μ p}
   …