OAI/Analysis/Conductivity/Variational/UniformNormBound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.uniform_zero_norm_of_bound line 25
  2. lemma OAI.ScalarConductivity.nonlinearFirstPotential_fderiv_error_tendsto line 34
  3. lemma OAI.ScalarConductivity.scalar_cutoff_segment line 53
  4. lemma OAI.ScalarConductivity.nonlinear_phase_leading_positive line 64
  5. lemma OAI.ScalarConductivity.lineShift_hasFDerivAt line 106
  6. def OAI.ScalarConductivity.lineShiftGradientOperator line 111
  7. lemma OAI.ScalarConductivity.lineShiftGradientOperator_apply line 115
  8. lemma OAI.ScalarConductivity.nonlinearLineShift_fderiv line 119
  9. lemma OAI.ScalarConductivity.nonlinearLineShift_fderiv_error_tendsto line 137
  10. lemma OAI.ScalarConductivity.equiv_image_set_of_eq_off line 150
  11. theorem OAI.ScalarConductivity.exists_local_phase_diffeomorphisms line 164