MovingExponentialWeights.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Variation of differences of exponential endpoint weights. The bound is polynomial in logarithmic variation; it never exponentiates the size of a top's logarithmic loss.

def OAI.LipschitzHilbert.complexSegment line 13
theorem OAI.LipschitzHilbert.complexSegment_re_le line 15
theorem OAI.LipschitzHilbert.complexSegment_difference line 22
theorem OAI.LipschitzHilbert.hasDerivAt_complexSegment line 38

theorem OAI.LipschitzHilbert.exp_increment_difference_bound line 47

Source documentation

A four-point exponential estimate on a left half-plane. Only the uniform real-part bound is exponentiated.

theorem exp_increment_difference_bound (a b c d : ℂ) (C D : ℝ)
    (ha : a.re ≤ C) (hb : b.re ≤ C) (hc : c.re ≤ C) (hd : d.re ≤ C)
    (hac : ‖c-a‖ ≤ D) (hbd : ‖d-b‖ ≤ D) :
    ‖(Complex.exp d-Complex.exp c)-(Complex.exp b-Complex.exp a)‖ ≤
      Real.exp C*(‖(d-c)-(b-a)‖+D*‖b-a‖) := by
…

theorem OAI.LipschitzHilbert.exponential_sequence_difference_variation line 93

Source documentation

The endpoint-plus-variation norm of a moving exponential difference is controlled by the logarithmic differences and their variation.

theorem exponential_sequence_difference_variation (L M : ℕ → ℂ) (N : ℕ)
    (C D V W : ℝ) (hD : 0 ≤ D)
    (hL : ∀ j ≤ N, (L j).re ≤ C) (hM : ∀ j ≤ N, (M j).re ≤ C)
    (hdiff : ∀ j ≤ N, ‖M j-L j‖ ≤ D)
    (hvar : (∑ j ∈ Finset.range N, ‖L (j+1)-L j‖) ≤ V)
    (hdvar : (∑ j ∈ Finset.range N, ‖(M (j+1)-M j)-(L (j+1)-L j)‖) ≤ W) :
    ‖Complex.exp (M N)-Complex.exp (L N)‖ +
      (∑ j ∈ Finset.range N,
        ‖(Complex.exp (M (j+1))-Complex.exp (L (j+1)))-
          (Complex.exp (M j)-Complex.exp (L j))‖) ≤
      Real.exp C*(D+W+D*V) := by
…