OAI/NumberTheory/JointDickman/Amplification/DiscardedRegionBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.discarded_region_integral_bound line 13

   Source documentation

   Young's inequality gives the needed two-endpoint estimate without introducing a separate square root of each Parseval bound.

   theorem discarded_region_integral_bound {F G H : ℝ → ℂ} {E : Set ℝ} {D : ℝ}
       (hE : MeasurableSet E) (hsub : E ⊆ Set.Ioc 0 1) (hD : 0 ≤ D)
       (hF : Continuous F) (hG : Continuous G)
       (hH : ∀ θ ∈ E, ‖H θ‖ ≤ D) :
       ‖∫ θ in E, F θ*G θ*H θ‖ ≤
         D/2*((∫ θ in (0 : ℝ)..1, ‖F θ‖^2)+(∫ θ in (0 : ℝ)..1, ‖G θ‖^2)) := by
   …