OAI/Probability/LogConcave/JetEstimates/WireStep.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.comp line 23
  2. lemma OAI.LogConcaveSampling.TensorEnergy.bound_identity line 34
  3. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.contract line 38
  4. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.entry_sq line 53
  5. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.trace_sq line 61
  6. def OAI.LogConcaveSampling.TensorEnergy.wireStep line 72
  7. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.wireStep line 76
  8. def OAI.LogConcaveSampling.TensorEnergy.circuit line 84
  9. lemma OAI.LogConcaveSampling.TensorEnergy.circuit_bound line 89
  10. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.trace_abs line 98
  11. theorem OAI.LogConcaveSampling.TensorEnergy.closed_wire_circuit_bound line 104
  12. lemma OAI.LogConcaveSampling.TensorEnergy.cut_bundle_card line 121
  13. abbrev OAI.LogConcaveSampling.TensorEnergy.Path line 128
  14. def OAI.LogConcaveSampling.TensorEnergy.pathWeight line 130
  15. lemma OAI.LogConcaveSampling.TensorEnergy.pathWeight_snoc line 134
  16. theorem OAI.LogConcaveSampling.TensorEnergy.circuit_path_expansion line 147