OAI/NumberTheory/Ostmann/Arithmetic/MovingPivotDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_pivot_cancellation_budget line 12

   Source documentation

   The cancellation cost is derived from the actual child-product and pivot ranges. The large common logarithmic center cancels exactly.

   theorem moving_pivot_cancellation_budget (v w HL HR d p T Δ E C : ℝ)
       (hv : |v| ≤ Real.exp E) (hw : |w| ≤ Real.exp E)
       (hHL : |HL| ≤ Real.exp (T + C)) (hHR : |HR| ≤ Real.exp (T + C))
       (hden : Real.exp (T - Δ - C) ≤ |d| * p) :
       |v * HR| + |w * HL| ≤ Real.exp (Real.log 2 + E + Δ + 2 * C) * (|d| * p) := by
   …

2. theorem OAI.Ostmann.moving_pivot_relative_derivative line 32

   Source documentation

   Relative derivatives are stable through a linear pivot, with precisely the cancellation factor supplied by the range estimate above.

   theorem moving_pivot_relative_derivative (a b d X Y dX dY p A D : ℝ)
       (hd : d ≠ 0) (hX : 0 ≤ X) (hY : 0 ≤ Y) (hD : 0 ≤ D)
       (hDX : |dX| ≤ D * X) (hDY : |dY| ≤ D * Y)
       (hcancel : |a * Y| + |b * X| ≤ A * |d| * p) :
       |(a * dY - b * dX) / d| ≤ A * D * p := by
   …

3. theorem OAI.Ostmann.MovingSlotReversal.realPivot_hasDerivAt line 56
4. theorem OAI.Ostmann.MovingSlotReversal.log_realPivot_derivative line 68

   Source documentation

   This is the derivative of the logarithm used by every internal smooth cutoff. It applies to the literal moving-pivot formula.

   theorem MovingSlotReversal.log_realPivot_derivative {σ : Type*}
       (step : MovingSlotReversal σ) (value : σ → ℕ)
       {L R : ℝ → ℝ} {x dL dR : ℝ} (hL : HasDerivAt L dL x) (hR : HasDerivAt R dR x)
       (hp : 0 < step.realPivot value (L x) (R x)) :
       HasDerivAt (fun z => Real.log (step.realPivot value (L z) (R z)))
         (step.realPivot value dL dR / step.realPivot value (L x) (R x)) x :=
   …

   Mentions: OAI.Ostmann.MovingSlotReversal

5. theorem OAI.Ostmann.MovingSlotReversal.log_realPivot_derivative_bound line 78

   Source documentation

   The logarithmic derivative costs at most the cancellation factor times the incoming logarithmic derivative bound.

   theorem MovingSlotReversal.log_realPivot_derivative_bound {σ : Type*}
       (step : MovingSlotReversal σ) (value : σ → ℕ)
       (X Y dX dY A D : ℝ) (hs : step.rootFrequency ≠ 0)
       (hu : MovingSlotReversal.naturalProduct value step.compensationSlots ≠ 0)
       (hX : 0 ≤ X) (hY : 0 ≤ Y) (hD : 0 ≤ D)
       (hDX : |dX| ≤ D * X) (hDY : |dY| ≤ D * Y)
       (hp : 0 < step.realPivot value X Y)
       (hcancel : |(step.leftFrequency : ℝ) *
           (MovingSlotReversal.naturalProduct value step.rightSlots : ℝ) * Y| +
         |(step.rightFrequency : ℝ) *
           (MovingSlotReversal.naturalProduct value step.leftSlots : ℝ) * X| ≤
         A * |(step.rootFrequency : ℝ) *
   …

   Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.MovingSlotReversal.naturalProduct