OAI/Analysis/Conductivity/Sobolev/IntervalTraceEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.integral_sq_le_mass_mul line 10
2. lemma OAI.ScalarConductivity.interval_integral_sq_le line 30
3. lemma OAI.ScalarConductivity.smooth_interval_poincare_point line 38
4. theorem OAI.ScalarConductivity.fourier_mode_trace_energy line 47