OAI/Analysis/LipschitzHilbert/Trees/SourceFiniteExponentialIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite sums of the exact packet-path exponentials may be integrated against bounded Hilbert-valued tests on a bounded exhaustion.

  1. theorem OAI.LipschitzHilbert.source_affine_exp_integrable line 17
  2. theorem OAI.LipschitzHilbert.source_integral_finset_affine_exp_entire line 31
  3. theorem OAI.LipschitzHilbert.source_integral_finite_exponential_pairing_entire line 48
  4. theorem OAI.LipschitzHilbert.source_integral_finite_exponential_pairing_entire_on line 70