GaussianTimeConvolution.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Summing the long-time source blocks in the same geometric envelope

theorem OAI.RegularPointCoordinates.half_convolution_le_three_quarters line 15

Source documentation

The displacement factor contributes one half per time block. Its convolution with a three-quarter envelope loses only a factor three.

theorem half_convolution_le_three_quarters (F : ℕ → ℝ)
    (hF : ∀ i, 0 ≤ F i) (hstep : ∀ i, (3 / 4 : ℝ) * F i ≤ F (i + 1)) (i : ℕ) :
    (∑ j ∈ Finset.range (i + 1), (1 / 2 : ℝ) ^ (i - j) * F j) ≤ 3 * F i := by
…

theorem OAI.RegularPointCoordinates.dyadicBochnerEnvelope_step line 32

Source documentation

Exact recurrence for the actual full-mass envelope.

theorem dyadicBochnerEnvelope_step (M : PositiveBilinearMeasure X E) (n : ℕ)
    (x : X) (R : ℝ) (i : ℕ) (v : E) :
    ⟪v, dyadicBochnerEnvelope M n x R (i + 1) v⟫_ℝ =
      (3 / 4 : ℝ) * ⟪v, dyadicBochnerEnvelope M n x R i v⟫_ℝ +
        ⟪v, dyadicBochnerMass M n x R (i + 1) v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.dyadicBochnerEnvelope, OAI.RegularPointCoordinates.dyadicBochnerMass

theorem OAI.RegularPointCoordinates.dyadicBochnerEnvelope_time_sum_le line 42

Source documentation

Summing all time blocks preserves the original full-mass envelope; no enlarged mass or new source hypothesis is introduced.

theorem dyadicBochnerEnvelope_time_sum_le (M : PositiveBilinearMeasure X E) (n : ℕ)
    (x : X) {R : ℝ} (hR : 0 ≤ R) (i : ℕ) (v : E) :
    (∑ j ∈ Finset.range (i + 1), (1 / 2 : ℝ) ^ (i - j) *
      ⟪v, dyadicBochnerEnvelope M n x R j v⟫_ℝ) ≤
        3 * ⟪v, dyadicBochnerEnvelope M n x R i v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.dyadicBochnerEnvelope