OAI/NumberTheory/Ostmann/Arithmetic/MovingLogLeaves.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.realLeafModuli line 9
2. def OAI.Ostmann.MovingSlotData.PivotControl line 19

   Source documentation

   The quantitative cancellation test at every actual internal node.

   def MovingSlotData.PivotControl {σ : Type*} (value : σ → ℕ) (A : ℝ) :
       {n : ℕ} → MovingSlotData σ n → ℝ → ℝ → Prop
     | _, .leaf _ _, _, _ => True
     | _, .node s CL CR u left right, L, R =>
         let step := MovingSlotData.step s CL CR u left right false
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotData.step

3. theorem OAI.Ostmann.positive_product_relative_derivative line 31
4. theorem OAI.Ostmann.MovingSlotData.realLeafModuli_derivative line 46

   Source documentation

   Each leaf modulus has logarithmic derivative at most 2*A^depth*D. The depth, rather than the number of leaves, controls the amplification.

   theorem MovingSlotData.realLeafModuli_derivative {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) {n : ℕ} (T : MovingSlotData σ n)
       (hf : T.Frequencies (· ≠ 0)) (A D : ℝ) (hA : 1 ≤ A) (hD : 0 ≤ D)
       {L R : ℝ → ℝ} {x dL dR : ℝ} (hL : HasDerivAt L dL x) (hR : HasDerivAt R dR x)
       (hL0 : 0 < L x) (hR0 : 0 < R x) (hdL : |dL| ≤ D * L x) (hdR : |dR| ≤ D * R x)
       (hcontrol : T.PivotControl value A (L x) (R x)) (i : TreeLeafIndex n) :
       ∃ dM : ℝ,
         HasDerivAt (fun z => T.realLeafModuli value (L z) (R z) i) dM x ∧
         0 < T.realLeafModuli value (L x) (R x) i ∧
         |dM| ≤ 2 * A ^ n * D * T.realLeafModuli value (L x) (R x) i := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex

5. theorem OAI.Ostmann.MovingSlotData.log_realLeafModuli_derivative line 96

   Source documentation

   In logarithmic coordinates the derivative bound no longer contains the large leaf modulus. This is the quantity needed for smooth cutoffs.

   theorem MovingSlotData.log_realLeafModuli_derivative {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) {n : ℕ} (T : MovingSlotData σ n)
       (hf : T.Frequencies (· ≠ 0)) (A D : ℝ) (hA : 1 ≤ A) (hD : 0 ≤ D)
       {L R : ℝ → ℝ} {x dL dR : ℝ} (hL : HasDerivAt L dL x) (hR : HasDerivAt R dR x)
       (hL0 : 0 < L x) (hR0 : 0 < R x) (hdL : |dL| ≤ D * L x) (hdR : |dR| ≤ D * R x)
       (hcontrol : T.PivotControl value A (L x) (R x)) (i : TreeLeafIndex n) :
       ∃ d : ℝ, HasDerivAt (fun z => Real.log (T.realLeafModuli value (L z) (R z) i)) d x ∧
         |d| ≤ 2 * A ^ n * D := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex