MajorArcDecomposition.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.MinorArc.centerSet line 11
Source documentation
Reduced centers in the unit interval, with bounded denominator.
```
def centerSet (Q : ℕ) : Set ℚ :=
…
```
theorem OAI.Problem337.MinorArc.finite_centerSet line 15
Source documentation
The reduced centers form a genuinely finite set.
```
theorem finite_centerSet (Q : ℕ) : (centerSet Q).Finite := by
…
```
Mentions: OAI.Problem337.MinorArc.centerSet
def OAI.Problem337.MinorArc.centers line 29
Source documentation
The canonical finite indexing set of reduced centers, with duplicates removed.
```
def centers (Q : ℕ) : Finset ℚ := (finite_centerSet Q).toFinset
```
Mentions: OAI.Problem337.MinorArc.finite_centerSet
theorem OAI.Problem337.MinorArc.mem_centers line 31
theorem OAI.Problem337.MinorArc.majorArcs_unit_eq_centers_union line 37
Source documentation
The exact finite reduced-center decomposition of the major region. Clipping keeps both endpoint arcs at zero and one without any convention loss.
```
theorem majorArcs_unit_eq_centers_union {Q N : ℕ} (hN : 2 ≤ N) :
    majorArcs Q N ∩ Set.Icc (0 : ℝ) 1 =
      ⋃ r ∈ centers Q, arc N r ∩ Set.Icc (0 : ℝ) 1 := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.MinorArc.centers, OAI.Problem337.MinorArc.arc
theorem OAI.Problem337.MinorArc.centers_pairwiseDisjoint line 52
Source documentation
Distinct clipped reduced arcs are disjoint in the usual major-arc scale.
```
theorem centers_pairwiseDisjoint {Q N : ℕ} (hQN : 2 * Q < N) :
    Set.PairwiseDisjoint (↑(centers Q) : Set ℚ)
      (fun r => arc N r ∩ Set.Icc (0 : ℝ) 1) := by
…
```
Mentions: OAI.Problem337.MinorArc.centers, OAI.Problem337.MinorArc.arc
theorem OAI.Problem337.MinorArc.integral_majorArcs_eq_sum line 63
Source documentation
Exact integration over major arcs is a finite sum over reduced centers. The only analytic premise is integrability of the actual integrand on [0,1].
```
theorem integral_majorArcs_eq_sum {Q N : ℕ} (hN : 2 ≤ N) (hQN : 2 * Q < N)
    (f : ℝ → ℂ) (hf : IntegrableOn f (Set.Icc (0 : ℝ) 1)) :
    (∫ x in majorArcs Q N ∩ Set.Icc (0 : ℝ) 1, f x) =
      ∑ r ∈ centers Q, ∫ x in arc N r ∩ Set.Icc (0 : ℝ) 1, f x := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.MinorArc.centers, OAI.Problem337.MinorArc.arc

theorem OAI.Problem337.MinorArc.integral_unit_eq_major_sum_add_minor line 77

Source documentation

The whole interval integral splits into the explicit reduced major-arc sum and its minor complement, with no implicit endpoint or overlap error.

theorem integral_unit_eq_major_sum_add_minor {Q N : ℕ}
    (hN : 2 ≤ N) (hQN : 2 * Q < N)
    (f : ℝ → ℂ) (hf : IntegrableOn f (Set.Icc (0 : ℝ) 1)) :
    (∫ x in Set.Icc (0 : ℝ) 1, f x) =
      (∑ r ∈ centers Q, ∫ x in arc N r ∩ Set.Icc (0 : ℝ) 1, f x) +
      ∫ x in Set.Icc (0 : ℝ) 1 \ majorArcs Q N, f x := by
…

Mentions: OAI.Problem337.MinorArc.centers, OAI.Problem337.MinorArc.arc, OAI.Problem337.MinorArc.majorArcs

theorem OAI.Problem337.MinorArc.integral_majorArcUnion_unit_eq_sum line 89

Source documentation

The same exact decomposition using the finite major region in the prime/AP approximation API.

theorem integral_majorArcUnion_unit_eq_sum {Q N : ℕ}
    (hN : 2 ≤ N) (hQN : 2 * Q < N)
    (f : ℝ → ℂ) (hf : IntegrableOn f (Set.Icc (0 : ℝ) 1)) :
    (∫ x in ThreePrimeAnalysis.majorArcUnion Q (1 / (N : ℝ)) ∩
      Set.Icc (0 : ℝ) 1, f x) =
      ∑ r ∈ centers Q, ∫ x in arc N r ∩ Set.Icc (0 : ℝ) 1, f x := by
…

Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion, OAI.Problem337.MinorArc.centers, OAI.Problem337.MinorArc.arc