OAI/Analysis/Conductivity/Variational/CrossingEstimates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.cutoff_exp_hasDerivAt line 10
  2. lemma OAI.ScalarConductivity.cutoff_exp_residual line 19
  3. lemma OAI.ScalarConductivity.crossing_cutoff_derivative_bounds line 34
  4. def OAI.ScalarConductivity.crossingResidualFirst line 57
  5. def OAI.ScalarConductivity.crossingResidualSecond line 60
  6. lemma OAI.ScalarConductivity.crossingResidualFirst_formula line 63
  7. lemma OAI.ScalarConductivity.crossingResidualSecond_formula line 69
  8. lemma OAI.ScalarConductivity.crossingResidualFirst_normalized line 76
  9. lemma OAI.ScalarConductivity.crossingResidualSecond_normalized line 82
  10. lemma OAI.ScalarConductivity.crossingResidualFirst_zero line 89
  11. lemma OAI.ScalarConductivity.crossingResidualSecond_zero line 98
  12. lemma OAI.ScalarConductivity.crossing_residual_bounds line 108
  13. lemma OAI.ScalarConductivity.crossing_mode_ratios line 138
  14. lemma OAI.ScalarConductivity.exists_small_crossing_scale line 155