OAI/Analysis/TriangularHilbert/SampledOutput.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularHilbert.Heat.cyclicKernelOutput line 11
  2. def OAI.TriangularHilbert.Heat.sampledIntegrand line 14
  3. def OAI.TriangularHilbert.Heat.sampledKernelOutput line 18
  4. lemma OAI.TriangularHilbert.Heat.sampledKernelOutput_eq_sum line 21
  5. lemma OAI.TriangularHilbert.Heat.gridLift_kernelOutput_eq line 37
  6. lemma OAI.TriangularHilbert.Heat.measurable_sampledIntegrand line 59
  7. lemma OAI.TriangularHilbert.Heat.measurable_sampledKernelOutput line 68
  8. lemma OAI.TriangularHilbert.Heat.sampledIntegrand_support_c line 72
  9. lemma OAI.TriangularHilbert.Heat.sampledIntegrand_support_z line 78
  10. lemma OAI.TriangularHilbert.Heat.sampledKernelOutput_support line 86