OAI/NumberTheory/CubicMoment/Transform/MetaplecticPoleContour.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicFirstMoment.simplePole_line_continuous line 14
2. lemma OAI.CubicFirstMoment.simplePole_line_integral line 25

   Source documentation

   The symmetric integral of a simple-pole kernel is an arctangent. Keeping its imaginary part exact avoids any conditionally convergent integral in the eventual contour shift.

   lemma simplePole_line_integral {c : ℝ} (hc : c ≠ 0) (T : ℝ) :
       (∫ t in -T..T, ((c:ℂ)+(t:ℂ)*Complex.I)⁻¹) = (2*Real.arctan (T/c):ℝ) := by
   …

3. lemma OAI.CubicFirstMoment.simplePole_line_tendsto_pos line 48
4. lemma OAI.CubicFirstMoment.simplePole_line_tendsto_neg line 58
5. def OAI.CubicFirstMoment.poleRegularPart line 68
6. lemma OAI.CubicFirstMoment.poleRegularPart_differentiableOn line 71
7. lemma OAI.CubicFirstMoment.poleRegularPart_eq line 81
8. lemma OAI.CubicFirstMoment.simplePole_horizontal_tendsto line 88

   Source documentation

   The horizontal edges of the subtracted constant pole tend to zero.

   lemma simplePole_horizontal_tendsto (a b c : ℝ) :
       Tendsto (fun T : ℝ => ∫ x in a..b,
         ((x:ℂ)+(T:ℂ)*Complex.I-(c:ℂ))⁻¹) atTop (𝓝 0) := by
   …

9. lemma OAI.CubicFirstMoment.poleRegularPart_vertical_limit line 103
10. theorem OAI.CubicFirstMoment.mellin_single_pole_shift line 140

    Source documentation

    A one-pole contour shift with both horizontal limits kept explicit. The removable part is constructed from a divided difference, and the residue contribution comes from the proved arctangent kernel limits.

    theorem mellin_single_pole_shift (M g : ℂ → ℂ) (ρ : ℂ) {a b c : ℝ}
        (hac : a < c) (hcb : c < b) (hM : Differentiable ℂ M)
        (hg : DifferentiableOn ℂ g (closedVerticalStrip a b))
        (ha : Integrable (fun t : ℝ => M ((a:ℂ)+(t:ℂ)*Complex.I)*
          (g ((a:ℂ)+(t:ℂ)*Complex.I)+ρ/((a:ℂ)+(t:ℂ)*Complex.I-(c:ℂ)))))
        (hb : Integrable (fun t : ℝ => M ((b:ℂ)+(t:ℂ)*Complex.I)*
          (g ((b:ℂ)+(t:ℂ)*Complex.I)+ρ/((b:ℂ)+(t:ℂ)*Complex.I-(c:ℂ)))))
        (hTop : Tendsto (fun T : ℝ => ∫ x in a..b,
          poleRegularPart M g ρ c ((x:ℂ)+(T:ℂ)*Complex.I)) atTop (𝓝 0))
        (hBot : Tendsto (fun T : ℝ => ∫ x in a..b,
          poleRegularPart M g ρ c ((x:ℂ)-(T:ℂ)*Complex.I)) atTop (𝓝 0)) :
        (∫ t : ℝ, M ((b:ℂ)+(t:ℂ)*Complex.I)*
    …

    Mentions: OAI.CubicFirstMoment.closedVerticalStrip, OAI.CubicFirstMoment.poleRegularPart

11. lemma OAI.CubicFirstMoment.poleRegularPart_edge_bound line 180
12. theorem OAI.CubicFirstMoment.mellin_single_pole_shift_of_majorant line 212

    Source documentation

    A vanishing majorant for the original meromorphic integrand supplies the regularized horizontal limits required by the residue calculation.

    theorem mellin_single_pole_shift_of_majorant (M g : ℂ → ℂ) (ρ : ℂ) {a b c : ℝ}
        (hac : a < c) (hcb : c < b) (hM : Differentiable ℂ M)
        (hg : DifferentiableOn ℂ g (closedVerticalStrip a b))
        (ha : Integrable (fun t : ℝ => M ((a:ℂ)+(t:ℂ)*Complex.I)*
          (g ((a:ℂ)+(t:ℂ)*Complex.I)+ρ/((a:ℂ)+(t:ℂ)*Complex.I-(c:ℂ)))))
        (hb : Integrable (fun t : ℝ => M ((b:ℂ)+(t:ℂ)*Complex.I)*
          (g ((b:ℂ)+(t:ℂ)*Complex.I)+ρ/((b:ℂ)+(t:ℂ)*Complex.I-(c:ℂ)))))
        (H : ℝ → ℝ) (hHt : Tendsto H atTop (𝓝 0)) (hHb : Tendsto H atBot (𝓝 0))
        (hH : ∀ x ∈ Icc a b, ∀ t : ℝ, 1 ≤ |t| →
          ‖M ((x:ℂ)+(t:ℂ)*Complex.I)*
            (g ((x:ℂ)+(t:ℂ)*Complex.I)+ρ/((x:ℂ)+(t:ℂ)*Complex.I-(c:ℂ)))‖ ≤ H t) :
        (∫ t : ℝ, M ((b:ℂ)+(t:ℂ)*Complex.I)*
    …

    Mentions: OAI.CubicFirstMoment.closedVerticalStrip