OAI/Analysis/KadisonKastler/RealLaplaceUniqueness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exp_positivePart_integrable line 15
2. theorem OAI.KadisonKastler.exp_density_integrable line 25
3. theorem OAI.KadisonKastler.mgf_density line 33
4. theorem OAI.KadisonKastler.ae_zero_of_local_laplace line 45

   Source documentation

   A real coefficient with an open interval of exponential integrability is zero almost everywhere if all its Laplace values in that interval vanish.

   theorem ae_zero_of_local_laplace (f : ℝ → ℝ) (hf : Measurable f)
       {a : ℝ} (ha : 0 < a)
       (hi : ∀ s ∈ Ioo (-a) a, Integrable (fun t => Real.exp (s * t) * f t))
       (hz : ∀ s ∈ Ioo (-a) a, (∫ t, Real.exp (s * t) * f t) = 0) :
       f =ᵐ[volume] 0 := by
   …

5. theorem OAI.KadisonKastler.zero_of_local_laplace line 101

   Source documentation

   For continuous coefficients, the conclusion holds at every real parameter.

   theorem zero_of_local_laplace (f : ℝ → ℝ) (hf : Continuous f)
       {a : ℝ} (ha : 0 < a)
       (hi : ∀ s ∈ Ioo (-a) a, Integrable (fun t => Real.exp (s * t) * f t))
       (hz : ∀ s ∈ Ioo (-a) a, (∫ t, Real.exp (s * t) * f t) = 0) :
       f = 0 :=
   …