HeatBlockIntegrals.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Integrating the uniform bounds on source time blocks

theorem OAI.RegularPointCoordinates.scaled_block_integral_norm_le line 16

Source documentation

A scaled pointwise block bound gives the same integral budget on any time interval of length at most the square of that scale.

theorem scaled_block_integral_norm_le {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] {f : ℝ → E} {a b s B : ℝ}
    (hs : 0 < s) (hab : a ≤ b) (hlength : b - a ≤ s ^ 2) (hB : 0 ≤ B)
    (hbound : ∀ t ∈ Ioc a b, s ^ 2 * ‖f t‖ ≤ B) :
    ‖∫ t in a..b, f t‖ ≤ B := by
…

theorem OAI.RegularPointCoordinates.short_time_integral_norm_le line 35

Source documentation

The full short-time interval consumes exactly one source-envelope budget, once the uniform scaled estimate is available.

theorem short_time_integral_norm_le {f : ℝ → ℝ} {s B : ℝ}
    (hs : 0 < s) (hB : 0 ≤ B)
    (hbound : ∀ t, 0 < t → t ≤ s ^ 2 → s ^ 2 * |f t| ≤ B) :
    |∫ t in (0 : ℝ)..s ^ 2, f t| ≤ B := by
…

theorem OAI.RegularPointCoordinates.dyadic_time_integral_norm_le line 45

Source documentation

The quarter-square to square interval is the actual long-time block.

theorem dyadic_time_integral_norm_le {f : ℝ → ℝ} {s B : ℝ}
    (hs : 0 < s) (hB : 0 ≤ B)
    (hbound : ∀ t ∈ Icc (s ^ 2 / 4) (s ^ 2), s ^ 2 * |f t| ≤ B) :
    |∫ t in (s ^ 2 / 4)..s ^ 2, f t| ≤ B := by
…