OAI/Analysis/Steinitz/KernelConvexity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Convexity and norm inequalities for Gaussian kernels.

  1. lemma OAI.HeatL2.le_of_shifted_pow_le_const_mul_pow line 13
  2. lemma OAI.HeatL2.kernel_norm_logconcave_of_pathMass line 29
  3. lemma OAI.HeatL2.pathMass_logconcave_haar line 67
  4. lemma OAI.GaussianKernel.kernel_value_continuous line 110
  5. lemma OAI.GaussianKernel.kernel_value_pos line 113
  6. lemma OAI.GaussianKernel.kernel_value_logconcave line 117
  7. lemma OAI.GaussianKernel.compressed_norm_logconcave line 129