OAI/Analysis/LipschitzHilbert/Trees/ResidualOscillation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.packetPrefix line 15
2. theorem OAI.LipschitzHilbert.interval_packet_sum_le line 18
3. theorem OAI.LipschitzHilbert.boundary_segment_amplitude_le_oscillation line 27

   Source documentation

   The coefficient-variation estimate uses the full root mass ratio. The packet maximum itself is restricted to the current segment.

   theorem boundary_segment_amplitude_le_oscillation {E : Type*} [NormedAddCommGroup E]
       [NormedSpace ℂ E] (n m : ℕ → ℝ) (z : ℕ → ℂ) (f : ℕ → E)
       (start N K H a b : ℕ) (power lower Z : ℝ)
       (hstart : start ≤ N) (ha : a ≤ start) (hb : N + 1 ≤ b) (hbH : b ≤ H)
       (hpower : 0 ≤ power) (hlower : 0 < lower) (hZ : 0 ≤ Z)
       (hn : ∀ j ≤ N, lower ≤ n j) (hmono : AntitoneOn n (Set.Iic N))
       (hm : ∀ j < N, n (j + 1) ≤ m j ∧ m j ≤ n (j + 1 - K))
       (hz0 : ∀ j < N, 0 ≤ (z j).re) (hz : ∀ j < N, ‖z j‖ ≤ Z) :
       ‖∑ j ∈ Finset.Ico start (N + 1),
         segmentWeight n (boundaryLog n m) z power start j • f j‖ ≤
         (lower ^ (-power) * (1 + (power + Z * K) * Real.log (n 0 / n N))) *
           intervalOscillation (packetPrefix f) H a b := by
   …

   Mentions: OAI.LipschitzHilbert.segmentWeight, OAI.LipschitzHilbert.boundaryLog, OAI.LipschitzHilbert.intervalOscillation, OAI.LipschitzHilbert.packetPrefix