PeriodicMajorArcIntegrals.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.MinorArc.integral_majorArcs_inter_eq_sum line 13
Source documentation
Exact disjoint finite-sum decomposition on any measurable integration set. The normalized zero center retains both pieces crossing the unit endpoints.
```
theorem integral_majorArcs_inter_eq_sum {Q N : ℕ} (hQN : 2 * Q < N)
    {E : Set ℝ} (hE : MeasurableSet E) (f : ℝ → ℂ)
    (hf : IntegrableOn f (majorArcs Q N ∩ E)) :
    (∫ x in majorArcs Q N ∩ E, f x) =
      ∑ r ∈ normalizedCenters Q, ∫ x in periodicArc N r ∩ E, f x := by
…
```
Mentions: OAI.Problem337.MinorArc.majorArcs, OAI.Problem337.MinorArc.normalizedCenters, OAI.Problem337.MinorArc.periodicArc
theorem OAI.Problem337.MinorArc.integral_eq_majorArc_sum_add_minor line 40
Source documentation
The full integral separates into the exact finite major-arc sum and the minor-arc remainder; no endpoint contribution is omitted.
```
theorem integral_eq_majorArc_sum_add_minor {Q N : ℕ} (hQN : 2 * Q < N)
    {E : Set ℝ} (hE : MeasurableSet E) (f : ℝ → ℂ)
    (hf : IntegrableOn f E) :
    (∫ x in E, f x) =
      (∑ r ∈ normalizedCenters Q, ∫ x in periodicArc N r ∩ E, f x) +
        ∫ x in E \ majorArcs Q N, f x := by
…
```
Mentions: OAI.Problem337.MinorArc.normalizedCenters, OAI.Problem337.MinorArc.periodicArc, OAI.Problem337.MinorArc.majorArcs
theorem OAI.Problem337.MinorArc.integral_unit_eq_majorArc_sum_add_minor line 54
Source documentation
Continuous circle-method integrands automatically meet the integrability hypothesis on the compact unit interval.
```
theorem integral_unit_eq_majorArc_sum_add_minor {Q N : ℕ} (hQN : 2 * Q < N)
    (f : ℝ → ℂ) (hf : Continuous f) :
    (∫ x in Icc (0 : ℝ) 1, f x) =
      (∑ r ∈ normalizedCenters Q,
        ∫ x in periodicArc N r ∩ Icc (0 : ℝ) 1, f x) +
        ∫ x in Icc (0 : ℝ) 1 \ majorArcs Q N, f x := by
…
```
Mentions: OAI.Problem337.MinorArc.normalizedCenters, OAI.Problem337.MinorArc.periodicArc, OAI.Problem337.MinorArc.majorArcs