OAI/Analysis/Conductivity/Variational/DerivativeEquiv.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.fderiv_equiv_symm_comp line 15
  2. lemma OAI.ScalarConductivity.fderiv_equiv_comp_symm line 22
  3. def OAI.ScalarConductivity.derivativeEquiv line 28
  4. lemma OAI.ScalarConductivity.fderiv_equiv_det_ne_zero line 33
  5. lemma OAI.ScalarConductivity.piolaFlux_derivative_pairing line 41
  6. def OAI.ScalarConductivity.smoothEquivHomeomorph line 53
  7. lemma OAI.ScalarConductivity.piolaFlux_hasCompactSupport line 57
  8. lemma OAI.ScalarConductivity.piolaFlux_zero_pairing line 67
  9. lemma OAI.ScalarConductivity.equiv_mapsTo_of_fixed_compl line 81
  10. def OAI.ScalarConductivity.flatPulse line 101
  11. lemma OAI.ScalarConductivity.flatPulse_smooth line 104
  12. lemma OAI.ScalarConductivity.flatPulse_zero_left line 108
  13. lemma OAI.ScalarConductivity.flatPulse_zero_right line 114
  14. lemma OAI.ScalarConductivity.flatPulse_one line 119
  15. lemma OAI.ScalarConductivity.flatPulse_bounds line 125
  16. lemma OAI.ScalarConductivity.flatPulse_support line 136
  17. def OAI.ScalarConductivity.periodicPulse line 145
  18. lemma OAI.ScalarConductivity.pulse_translates_locallyFinite line 147
  19. lemma OAI.ScalarConductivity.periodicPulse_smooth line 157
  20. lemma OAI.ScalarConductivity.periodicPulse_periodic line 164
  21. lemma OAI.ScalarConductivity.periodicPulse_eq line 172
  22. lemma OAI.ScalarConductivity.periodicPulse_bounds line 186
  23. lemma OAI.ScalarConductivity.smoothStep_integral line 198
  24. lemma OAI.ScalarConductivity.flatPulse_integral line 226
  25. lemma OAI.ScalarConductivity.periodicPulse_integral line 238
  26. theorem OAI.ScalarConductivity.exists_two_state_wave line 245