MajorArcBridge.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.MinorArc.displayed_fraction_den_le line 10
Source documentation
Reduction of a displayed natural fraction cannot increase its denominator.
```
theorem displayed_fraction_den_le (a q : ℕ) (hq : 0 < q) :
    ((a : ℚ) / q).den ≤ q := by
…
```
theorem OAI.Problem337.MinorArc.finite_majorArcs_subset line 18
Source documentation
The finite nonreduced union is contained in the reduced-rational union. No restriction to the unit interval is needed in this direction.
```
theorem finite_majorArcs_subset (Q N : ℕ) :
    ThreePrimeAnalysis.majorArcUnion Q (1 / (N : ℝ)) ⊆ majorArcs Q N := by
…
```
Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion, OAI.Problem337.MinorArc.majorArcs
theorem OAI.Problem337.MinorArc.majorArcs_unit_eq_finite line 40
Source documentation
On the unit interval the reduced-rational and finite nonreduced major arcs coincide, so their Dirichlet and integration APIs can be combined.
```
theorem majorArcs_unit_eq_finite {Q N : ℕ} (hN : 2 ≤ N) :
    majorArcs Q N ∩ Set.Icc (0 : ℝ) 1 =
      ThreePrimeAnalysis.majorArcUnion Q (1 / (N : ℝ)) ∩ Set.Icc (0 : ℝ) 1 :=
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.ThreePrimeAnalysis.majorArcUnion

theorem OAI.Problem337.MinorArc.norm_integral_majorArcs_unit_le line 47

Source documentation

The exact bridge transfers the uniform integration budget to the actual reduced-rational major arcs used in Dirichlet extraction.

theorem norm_integral_majorArcs_unit_le {Q N : ℕ} (hN : 2 ≤ N)
    {B : ℝ} (hB : 0 ≤ B) (f : ℝ → ℂ)
    (hf : ∀ x ∈ majorArcs Q N ∩ Set.Icc (0 : ℝ) 1, ‖f x‖ ≤ B) :
    ‖∫ x in majorArcs Q N ∩ Set.Icc (0 : ℝ) 1, f x‖ ≤
      4 * B * (Q : ℝ) / N := by
…

Mentions: OAI.Problem337.MinorArc.majorArcs

theorem OAI.Problem337.MinorArc.norm_integral_cubic_majorArcs_unit_error_le line 61

Source documentation

The cubic major-arc error bound in the reduced-rational interface.

theorem norm_integral_cubic_majorArcs_unit_error_le {Q N : ℕ} (hN : 2 ≤ N)
    {B ε : ℝ} (hB : 0 ≤ B) (hε : 0 ≤ ε) (f g phase : ℝ → ℂ)
    (hf : ∀ x ∈ majorArcs Q N ∩ Set.Icc (0 : ℝ) 1, ‖f x‖ ≤ B)
    (hg : ∀ x ∈ majorArcs Q N ∩ Set.Icc (0 : ℝ) 1, ‖g x‖ ≤ B)
    (herr : ∀ x ∈ majorArcs Q N ∩ Set.Icc (0 : ℝ) 1, ‖f x - g x‖ ≤ ε)
    (hphase : ∀ x ∈ majorArcs Q N ∩ Set.Icc (0 : ℝ) 1, ‖phase x‖ ≤ 1) :
    ‖∫ x in majorArcs Q N ∩ Set.Icc (0 : ℝ) 1,
      (f x ^ 3 - g x ^ 3) * phase x‖ ≤ 12 * (Q : ℝ) * B ^ 2 * ε / N := by
…

Mentions: OAI.Problem337.MinorArc.majorArcs