WeightedConvolution.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted convolution estimates for changing inverse metrics

theorem OAI.RegularPointCoordinates.positive_form_sum_le_card line 14

Source documentation

A positive quadratic form of a finite sum is bounded by the number of terms times their total energy. Degeneracy of the form is allowed.

theorem positive_form_sum_le_card {E ι : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] (D : E →L[ℝ] E) (hD : D.IsPositive)
    (s : Finset ι) (v : ι → E) :
    ⟪∑ j ∈ s, v j, D (∑ j ∈ s, v j)⟫_ℝ ≤
      (s.card : ℝ) * ∑ j ∈ s, ⟪v j, D (v j)⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.triangular_sum_le_square line 38

Source documentation

Reindex the lower triangle by the lag and initial index, then enlarge to the full square.

theorem triangular_sum_le_square (k : ℕ) (f : ℕ → ℕ → ℝ)
    (hf : ∀ m j, 0 ≤ f m j) :
    (∑ i ∈ Finset.range k, ∑ j ∈ Finset.range (i + 1), f (i - j) j) ≤
      ∑ m ∈ Finset.range k, ∑ j ∈ Finset.range k, f m j := by
…

theorem OAI.RegularPointCoordinates.sliding_interval_sum_le line 74

Source documentation

Each location belongs to at most m forward intervals of length m.

theorem sliding_interval_sum_le (k m : ℕ) (b : ℕ → ℝ) (hb : ∀ l, 0 ≤ b l) :
    (∑ j ∈ Finset.range k, ∑ l ∈ Finset.Ico j (min k (j + m)), b l) ≤
      (m : ℝ) * ∑ l ∈ Finset.range k, b l := by
…

theorem OAI.RegularPointCoordinates.weighted_interval_convolution_le line 114

Source documentation

The interval-convolution coefficient is the first moment of the lag kernel; no dependence on the final index remains.

theorem weighted_interval_convolution_le (k : ℕ) (w b : ℕ → ℝ)
    (hw : ∀ m, 0 ≤ w m) (hb : ∀ l, 0 ≤ b l) :
    (∑ i ∈ Finset.range k, ∑ j ∈ Finset.range (i + 1),
      w (i - j) * ∑ l ∈ Finset.Ico j i, b l) ≤
      (∑ m ∈ Finset.range k, (m : ℝ) * w m) * ∑ l ∈ Finset.range k, b l := by
…

theorem OAI.RegularPointCoordinates.weighted_stationary_convolution_le line 145

Source documentation

The stationary part of the triangular convolution has its ordinary geometric-series coefficient.

theorem weighted_stationary_convolution_le (k : ℕ) (w b : ℕ → ℝ)
    (hw : ∀ m, 0 ≤ w m) (hb : ∀ j, 0 ≤ b j) :
    (∑ i ∈ Finset.range k, ∑ j ∈ Finset.range (i + 1), w (i - j) * b j) ≤
      (∑ m ∈ Finset.range k, w m) * ∑ j ∈ Finset.range k, b j := by
…

def OAI.RegularPointCoordinates.geometricIntervalConstant line 155
Source documentation
The constant controlling intervals with exponentially decaying lags.
```
noncomputable def geometricIntervalConstant (rho : ℝ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.geometricIntervalConstant_nonneg line 158
theorem OAI.RegularPointCoordinates.weighted_geometric_interval_convolution_le line 162
theorem OAI.RegularPointCoordinates.weighted_geometric_stationary_convolution_le line 177