OAI/NumberTheory/Ostmann/Arithmetic/MovingLeafAmplitude.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingDataWeight_unit_leaf_bound line 12
2. theorem OAI.Ostmann.movingDataWeight_unit_norm_le_one line 30

   Source documentation

   Removing the explicit compensation multipliers leaves a scalar amplitude of norm at most one whenever the actual leaf coefficients have that bound.

   theorem movingDataWeight_unit_norm_le_one {σ : Type*}
       (F : {k : ℕ} → MovingSlotData σ k → ℤ → ℂ)
       (hF : ∀ s regular, ‖F (.leaf s regular) s‖ ≤ 1)
       {n : ℕ} (T : MovingSlotData σ n) :
       ‖movingDataWeight F (fun _ _ _ _ => 1) T‖ ≤ 1 := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingDataWeight

3. theorem OAI.Ostmann.frequencyLeafWeight_pair_projection line 41
4. theorem OAI.Ostmann.movingDataWeight_pair_unit_leaf_bound line 61