HyperbolaCorrelation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.HyperbolaCorrelation.product_support_iff line 11

Source documentation

The common support of two columns cut off by a product bound.

theorem product_support_iff (X m n₁ n₂ : ℕ) (hn : 0 < max n₁ n₂) :
    (m * n₁ ≤ X ∧ m * n₂ ≤ X) ↔ m ≤ X / max n₁ n₂ := by
…

theorem OAI.Problem337.HyperbolaCorrelation.filter_common_support line 17
Source documentation
Intersecting two hyperbolic columns leaves an ordinary integer interval. Empty intervals and a zero value of one of the two column indices are allowed.
```
theorem filter_common_support (X L U n₁ n₂ : ℕ) (hn : 0 < max n₁ n₂) :
    (Finset.Icc L U).filter (fun m => m * n₁ ≤ X ∧ m * n₂ ≤ X) =
      Finset.Icc L (min U (X / max n₁ n₂)) := by
…
```

theorem OAI.Problem337.HyperbolaCorrelation.cutoff_correlation line 26

Source documentation

Exact correlation identity for arbitrary complex hyperbolic columns.

theorem cutoff_correlation (X L U n₁ n₂ : ℕ) (hn : 0 < max n₁ n₂)
    (f g : ℕ → ℂ) :
    (∑ m ∈ Finset.Icc L U,
      (if m * n₁ ≤ X then f m else 0) *
        conj (if m * n₂ ≤ X then g m else 0)) =
      ∑ m ∈ Finset.Icc L (min U (X / max n₁ n₂)), f m * conj (g m) := by
…

def OAI.Problem337.HyperbolaCorrelation.phase line 38
Source documentation
The standard real-frequency complex phase.
```
def phase (x : ℝ) : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)
```
theorem OAI.Problem337.HyperbolaCorrelation.norm_phase line 40
theorem OAI.Problem337.HyperbolaCorrelation.phase_sub line 43
def OAI.Problem337.HyperbolaCorrelation.column line 51
Source documentation
A column of a bilinear exponential sum with its actual hyperbolic support.
```
def column (α : ℝ) (X n m : ℕ) : ℂ :=
…
```
theorem OAI.Problem337.HyperbolaCorrelation.column_correlation line 57
Source documentation
The off-diagonal correlation is a geometric exponential sum on one interval, not a sum over an arbitrary subset. Differences are taken in ℝ, so negative frequencies are retained rather than truncated by natural subtraction.
```
theorem column_correlation (α : ℝ) (X L U n₁ n₂ : ℕ)
    (hn : 0 < max n₁ n₂) :
    (∑ m ∈ Finset.Icc L U, column α X n₁ m * conj (column α X n₂ m)) =
      ∑ m ∈ Finset.Icc L (min U (X / max n₁ n₂)),
        phase (α * (m : ℝ) * ((n₁ : ℝ) - (n₂ : ℝ))) := by
…
```
Mentions: OAI.Problem337.HyperbolaCorrelation.column, OAI.Problem337.HyperbolaCorrelation.phase

theorem OAI.Problem337.HyperbolaCorrelation.column_diagonal line 71

Source documentation

Diagonal correlations count the surviving rows exactly.

theorem column_diagonal (α : ℝ) (X L U n : ℕ) (hn : 0 < n) :
    (∑ m ∈ Finset.Icc L U, column α X n m * conj (column α X n m)) =
      ((Finset.Icc L (min U (X / n))).card : ℂ) := by
…

Mentions: OAI.Problem337.HyperbolaCorrelation.column

theorem OAI.Problem337.HyperbolaCorrelation.norm_column_le_one line 79
Source documentation
Unit modulus survives restriction, the hypothesis used in finite Type-II Cauchy--Schwarz estimates.
```
theorem norm_column_le_one (α : ℝ) (X n m : ℕ) : ‖column α X n m‖ ≤ 1 := by
…
```
Mentions: OAI.Problem337.HyperbolaCorrelation.column

theorem OAI.Problem337.HyperbolaCorrelation.weighted_column_correlation line 84

Source documentation

Constant column weights factor out before the geometric estimate.

theorem weighted_column_correlation (α : ℝ) (X L U n₁ n₂ : ℕ)
    (hn : 0 < max n₁ n₂) (b₁ b₂ : ℂ) :
    (∑ m ∈ Finset.Icc L U,
      (b₁ * column α X n₁ m) * conj (b₂ * column α X n₂ m)) =
      (b₁ * conj b₂) *
        ∑ m ∈ Finset.Icc L (min U (X / max n₁ n₂)),
          phase (α * (m : ℝ) * ((n₁ : ℝ) - (n₂ : ℝ))) := by
…

Mentions: OAI.Problem337.HyperbolaCorrelation.column, OAI.Problem337.HyperbolaCorrelation.phase

theorem OAI.Problem337.HyperbolaCorrelation.norm_weighted_column_correlation line 98

Source documentation

The weighted-correlation norm has precisely the product of the two weights.

theorem norm_weighted_column_correlation (α : ℝ) (X L U n₁ n₂ : ℕ)
    (hn : 0 < max n₁ n₂) (b₁ b₂ : ℂ) :
    ‖∑ m ∈ Finset.Icc L U,
      (b₁ * column α X n₁ m) * conj (b₂ * column α X n₂ m)‖ =
      ‖b₁‖ * ‖b₂‖ *
        ‖∑ m ∈ Finset.Icc L (min U (X / max n₁ n₂)),
          phase (α * (m : ℝ) * ((n₁ : ℝ) - (n₂ : ℝ)))‖ := by
…

Mentions: OAI.Problem337.HyperbolaCorrelation.column, OAI.Problem337.HyperbolaCorrelation.phase