OAI/Probability/LogConcave/JetEstimates/Extension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LogConcaveSampling.Appell.actual_jet_cumulant_energy line 27
2. def OAI.LogConcaveSampling.TensorEnergy.zeroExtension line 52
3. lemma OAI.LogConcaveSampling.TensorEnergy.zeroExtension_apply line 57
4. lemma OAI.LogConcaveSampling.TensorEnergy.dot_zeroExtension line 62
5. lemma OAI.LogConcaveSampling.TensorEnergy.energy_zeroExtension line 71
6. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.submatrix line 77