RealTypeI.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.RealTypeI.geometric_envelope_le_truncated_real line 13
lemma OAI.Problem337.RealTypeI.geometric_envelope_le_truncated line 28
Source documentation
The geometric envelope is bounded by the reciprocal-distance envelope used in the rational-approximation argument, also at an integer frequency.
```
lemma geometric_envelope_le_truncated (t : ℝ) (M H : ℕ) (hMH : M ≤ H) :
    RealPhase.envelope M t ≤ truncatedInv (H : ℝ) (intDistance t) := by
…
```
Mentions: OAI.Problem337.RealPhase.envelope

theorem OAI.Problem337.RealTypeI.sum_norm_phase_sums_le line 34

Source documentation

Actual near-rational Type I estimate on any integer interval, allowing different inner lengths, starting points and constant phases at every index.

theorem sum_norm_phase_sums_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (L : ℤ) (N H : ℕ) (length : ℤ → ℕ) (start shift : ℤ → ℝ)
    (hlength : ∀ n ∈ Finset.Ico L (L + N), length n ≤ H) :
    (∑ n ∈ Finset.Ico L (L + N),
      ‖∑ j ∈ Finset.range (length n),
        RealPhase.phase ((α * (n : ℝ)) * (start n + j) + shift n)‖) ≤
      (2 * (N : ℝ) / q + 1) *
        (2 * (H : ℝ) + 4 * (q : ℝ) * (1 + Real.log (2 * (q : ℝ)))) := by
…

Mentions: OAI.Problem337.RealPhase.phase

theorem OAI.Problem337.RealTypeI.norm_weighted_phase_sums_le line 56

Source documentation

Bounded coefficients and hyperbolic or otherwise varying inner intervals require no extra cancellation hypothesis.

theorem norm_weighted_phase_sums_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (L : ℤ) (N H : ℕ) (length : ℤ → ℕ) (start shift : ℤ → ℝ)
    (hlength : ∀ n ∈ Finset.Ico L (L + N), length n ≤ H)
    (weight : ℤ → ℂ) (W : ℝ) (hW : 0 ≤ W)
    (hweight : ∀ n ∈ Finset.Ico L (L + N), ‖weight n‖ ≤ W) :
    ‖∑ n ∈ Finset.Ico L (L + N), weight n *
      ∑ j ∈ Finset.range (length n),
        RealPhase.phase ((α * (n : ℝ)) * (start n + j) + shift n)‖ ≤
      W * ((2 * (N : ℝ) / q + 1) *
…

Mentions: OAI.Problem337.RealPhase.phase

def OAI.Problem337.RealTypeI.hyperbolicCost line 88
Source documentation
The explicit scalar cost of a hyperbolic Type I sum.
```
def hyperbolicCost (X : ℝ) (M q : ℕ) : ℝ :=
…
```

theorem OAI.Problem337.RealTypeI.sum_norm_hyperbolic_phase_sums_le line 94

Source documentation

The actual geometric sums with inner lengths at most X/n have the power-saving hyperbolic cost, rather than the ineffective common-cap cost.

theorem sum_norm_hyperbolic_phase_sums_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (X : ℝ) (hX : 0 ≤ X) (M : ℕ) (length : ℤ → ℕ) (start shift : ℤ → ℝ)
    (hlength : ∀ n ∈ Finset.Icc 1 (M : ℤ), (length n : ℝ) ≤ X / (n : ℝ)) :
    (∑ n ∈ Finset.Icc 1 (M : ℤ),
      ‖∑ j ∈ Finset.range (length n),
        RealPhase.phase ((α * (n : ℝ)) * (start n + j) + shift n)‖) ≤
      hyperbolicCost X M q := by
…

Mentions: OAI.Problem337.RealPhase.phase, OAI.Problem337.RealTypeI.hyperbolicCost

theorem OAI.Problem337.RealTypeI.norm_weighted_hyperbolic_phase_sums_le line 113

theorem OAI.Problem337.RealTypeI.sum_norm_log_hyperbolic_phase_sums_le line 146

Source documentation

Logarithmic inner weights cost at most 2 log(X+1) in the true hyperbolic Type I estimate. The zero-length case is included.

theorem sum_norm_log_hyperbolic_phase_sums_le
    (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
    (hcop : IsCoprime a (q : ℤ))
    (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
    (X : ℝ) (hX : 0 ≤ X) (M : ℕ) (length : ℤ → ℕ)
    (hlength : ∀ n ∈ Finset.Icc 1 (M : ℤ), (length n : ℝ) ≤ X / (n : ℝ)) :
    (∑ n ∈ Finset.Icc 1 (M : ℤ),
      ‖∑ j ∈ Finset.range (length n),
        (Real.log (j + 1 : ℕ) : ℂ) *
          RealPhase.phase ((α * (n : ℝ)) * (j + 1 : ℕ))‖) ≤
      (2 * Real.log (X + 1)) * hyperbolicCost X M q := by
…

Mentions: OAI.Problem337.RealPhase.phase, OAI.Problem337.RealTypeI.hyperbolicCost

theorem OAI.Problem337.RealTypeI.norm_weighted_log_hyperbolic_phase_sums_le line 199