WeaklySingularIntegral.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact integrability and norm bounds for an inverse-square-root Volterra kernel.

def OAI.ForcedComputation.WeaklySingular.inverseSqrt line 14
theorem OAI.ForcedComputation.WeaklySingular.inverseSqrt_nonneg line 16
theorem OAI.ForcedComputation.WeaklySingular.inverseSqrt_eq_rpow line 19
theorem OAI.ForcedComputation.WeaklySingular.inverseSqrt_intervalIntegrable line 24
theorem OAI.ForcedComputation.WeaklySingular.integral_inverseSqrt line 33
theorem OAI.ForcedComputation.WeaklySingular.inverseSqrt_sub_intervalIntegrable line 47
theorem OAI.ForcedComputation.WeaklySingular.integral_inverseSqrt_sub line 51

theorem OAI.ForcedComputation.WeaklySingular.intervalIntegrable_of_inverseSqrt_bound line 59

Source documentation

A measurable integrand dominated by the inverse-square-root kernel is integrable.

theorem intervalIntegrable_of_inverseSqrt_bound {t : ℝ} (ht : 0 ≤ t)
    (f : ℝ → E) (B : ℝ) (hm : AEStronglyMeasurable f (volume.restrict (Ioc 0 t)))
    (hb : ∀ s ∈ Ioc 0 t, ‖f s‖ ≤ B * inverseSqrt (t - s)) :
    IntervalIntegrable f volume 0 t := by
…

Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt

theorem OAI.ForcedComputation.WeaklySingular.norm_integral_le_inverseSqrt line 68
Source documentation
The exact square-root norm bound, including the zero-time endpoint.
```
theorem norm_integral_le_inverseSqrt {t : ℝ} (ht : 0 ≤ t) (f : ℝ → E) (B : ℝ)
    (hb : ∀ s ∈ Ioc 0 t, ‖f s‖ ≤ B * inverseSqrt (t - s)) :
    ‖∫ s in 0..t, f s‖ ≤ 2 * B * Real.sqrt t := by
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt
def OAI.ForcedComputation.WeaklySingular.volterra line 80
Source documentation
The actual Volterra integral for an operator-valued kernel and a source curve.
```
def volterra (K : ℝ → E →L[ℝ] E) (u : ℝ → E) (t : ℝ) : E :=
…
```
theorem OAI.ForcedComputation.WeaklySingular.norm_volterra_le line 83