OAI/NumberTheory/Ostmann/Arithmetic/WeightedFlagComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.weighted_flag_comparison_le line 14

   Source documentation

   A bounded function of finitely many flags changes only on their union of exceptional events. This estimate retains the original independent weights.

   theorem weighted_flag_comparison_le {X I : Type*} [Fintype X] [Fintype I]
       (w : X → ℝ) (hw : ∀ x, 0 ≤ w x)
       (f g : X → I → Bool) (bad : I → X → Prop) [∀ i x, Decidable (bad i x)]
       (heq : ∀ x, (∀ i, ¬bad i x) → f x = g x)
       (Ψ : X → (I → Bool) → ℂ) (B : ℝ) (hB : 0 ≤ B) (hΨ : ∀ x v, ‖Ψ x v‖ ≤ B) :
       ‖∑ x, (w x : ℂ) * (Ψ x (f x) - Ψ x (g x))‖ ≤
         2 * B * ∑ i, ∑ x, w x * if bad i x then 1 else 0 := by
   …