OAI/Combinatorics/SharpThreshold/ThresholdODE.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.hasDerivAt_log_odds line 10

   Source documentation

   The derivative of log odds, stated without any probability-specific definitions.

   theorem hasDerivAt_log_odds {μ : ℝ → ℝ} {d x : ℝ}
       (hd : HasDerivAt μ d x) (hpos : 0 < μ x) (hone : μ x < 1) :
       HasDerivAt (fun t => Real.log (μ t) - Real.log (1 - μ t))
         (d / (μ x * (1 - μ x))) x := by
   …

2. theorem OAI.Problem313.logistic_coordinate_width line 23

   Source documentation

   Integrating a logistic differential inequality by the mean value theorem. Continuity is needed on the closed interval, differentiability only in its interior.

   theorem logistic_coordinate_width {μ μ' : ℝ → ℝ} {a b C : ℝ}
       (hab : a ≤ b) (hcont : ContinuousOn μ (Set.Icc a b))
       (hμ : ∀ x ∈ Set.Icc a b, 0 < μ x ∧ μ x < 1)
       (hd : ∀ x ∈ Set.Ioo a b, HasDerivAt μ (μ' x) x)
       (hbound : ∀ x ∈ Set.Ioo a b, μ x * (1 - μ x) ≤ C * μ' x) :
       b - a ≤ C * ((Real.log (μ b) - Real.log (1 - μ b)) -
         (Real.log (μ a) - Real.log (1 - μ a))) := by
   …

3. theorem OAI.Problem313.logistic_width_of_hasDerivAt line 57

   Source documentation

   The symmetric endpoint form used in sharp-threshold estimates.

   theorem logistic_width_of_hasDerivAt {μ μ' : ℝ → ℝ} {a b C ε : ℝ}
       (hab : a ≤ b) (hε : 0 < ε) (hεone : ε < 1)
       (hcont : ContinuousOn μ (Set.Icc a b))
       (hμ : ∀ x ∈ Set.Icc a b, 0 < μ x ∧ μ x < 1)
       (hd : ∀ x ∈ Set.Ioo a b, HasDerivAt μ (μ' x) x)
       (hbound : ∀ x ∈ Set.Ioo a b, μ x * (1 - μ x) ≤ C * μ' x)
       (ha : μ a = ε) (hb : μ b = 1 - ε) :
       b - a ≤ 2 * C * Real.log ((1 - ε) / ε) := by
   …