OAI/Analysis/Conductivity/Variational/TransitionMajorant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.transitionMajorant line 14
2. lemma OAI.ScalarConductivity.transitionMajorant_smooth line 17
3. lemma OAI.ScalarConductivity.transitionMajorant_periodic line 23
4. lemma OAI.ScalarConductivity.transitionMajorant_bounds line 31
5. lemma OAI.ScalarConductivity.periodicPulse_shift_integral line 40
6. lemma OAI.ScalarConductivity.transitionMajorant_integral line 48
7. lemma OAI.ScalarConductivity.periodicPulse_impure_subset line 62
8. lemma OAI.ScalarConductivity.transitionMajorant_dominates line 80