OAI/Analysis/KadisonKastler/StripAverageUniqueness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The modular averaging kernels separate bounded continuous functions

  1. theorem OAI.KadisonKastler.stripAverageKernel_tilt line 14
  2. theorem OAI.KadisonKastler.stripAverageKernel_ne_zero line 22
  3. theorem OAI.KadisonKastler.zero_of_strip_averages line 29

    Source documentation

    A bounded continuous coefficient is determined by all the real exponential tilts of the strip averaging kernel.

    theorem zero_of_strip_averages {a : ℝ} (ha : 0 < a) (g : ℝ → ℂ)
    (hg : Continuous g) {B : ℝ} (hB : ∀ t, ‖g t‖ ≤ B)
    (hz : ∀ s ∈ Ioo (-a) a, (∫ t, stripAverageKernel a (s : ℂ) t * g t) = 0) :
    g = 0 := by
…

    Mentions: OAI.KadisonKastler.stripAverageKernel