OAI/Analysis/AffineBernstein/LogVariance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.inverseHessianPair_le_trace_gradientSquared line 17
2. lemma OAI.AffineBernstein.inverseHessianPair_eq_zero_outside_tsupport line 32
3. lemma OAI.AffineBernstein.continuous_cofactor_trace line 38
4. lemma OAI.AffineBernstein.integral_cofactor_trace_le_ball line 48
5. lemma OAI.AffineBernstein.log_energy_le_cutoff line 72