OAI/Analysis/LipschitzHilbert/Fourier/ReferenceLineCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.SlopeBox.referenceSlope line 15
2. theorem OAI.LipschitzHilbert.SlopeBox.measurable_referenceSlope line 18
3. theorem OAI.LipschitzHilbert.SlopeBox.referenceBinFunction_eq line 22
4. def OAI.LipschitzHilbert.SlopeBox.ReferencePopularCount line 38
5. theorem OAI.LipschitzHilbert.SlopeBox.reference_count_setup line 48

   Source documentation

   The actual angular bins on a reference line admit a common count and exponentially small planar exceptional set, independently of any list.

   theorem reference_count_setup (R : SlopeBox) (u : ℝ × ℝ → ℝ) (hu : Measurable u)
       {M : ℕ} (hM : 0 < M) {c K P θ : ℝ} (hc : 0 ≤ c) (hcM : c ≤ M)
       (hK : 0 ≤ K) (hP : 0 < P) (hθ : 0 < θ) :
       ∃ N : ℝ × ℝ → ℝ≥0∞, Measurable N ∧
         R.ReferencePopularCount u c P θ M N ∧
         ∀ lambda : ℝ, 0 ≤ lambda →
           (volume.prod volume).real (R.referenceException N K lambda) ≤
             384 * K * (K + P) * R.length * R.width *
               Real.exp (-θ * lambda / (240 * (1 + c))) := by
   …

   Mentions: OAI.LipschitzHilbert.SlopeBox