OAI/Analysis/BiholderTransport/Regularity/ActualParameter.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.ParameterVariation.abs_le_of_positive_barycentric line 17
  2. lemma OAI.WeakMTWTransport.ParameterVariation.exists_span_projection_bound line 42
  3. lemma OAI.WeakMTWTransport.ParameterVariation.exists_eventual_active_projection_bound line 80
  4. lemma OAI.WeakMTWTransport.ParameterVariation.exists_eventual_active_linear_bound line 111
  5. lemma OAI.WeakMTWTransport.ParameterVariation.projected_quadratic_lower line 149
  6. lemma OAI.WeakMTWTransport.ParameterVariation.norm_tendsto_zero_of_sq_bound line 162
  7. lemma OAI.WeakMTWTransport.ParameterVariation.weighted_parameter_bound line 171
  8. lemma OAI.WeakMTWTransport.ParameterVariation.compact_minimizers_tendsto line 265
  9. lemma OAI.WeakMTWTransport.ParameterVariation.perturbed_compact_minimizers_tendsto line 285
  10. lemma OAI.WeakMTWTransport.ParameterVariation.affine_minimum_derivative line 298
  11. lemma OAI.WeakMTWTransport.ParameterVariation.second_remainder_along_sqrt line 325
  12. def OAI.WeakMTWTransport.modifiedDatum line 348
  13. def OAI.WeakMTWTransport.modifiedExcess line 351
  14. lemma OAI.WeakMTWTransport.continuous_modifiedDatum line 355
  15. def OAI.WeakMTWTransport.parameterPenalty line 359
  16. def OAI.WeakMTWTransport.regularizedComparison line 361
  17. lemma OAI.WeakMTWTransport.modified_outer_decrease_bounds line 366
  18. lemma OAI.WeakMTWTransport.WeakMTW.hopfLax_minimizer_unique line 394
  19. lemma OAI.WeakMTWTransport.modified_active_split_contact line 419
  20. lemma OAI.WeakMTWTransport.WeakMTW.modified_pole_movement line 438
  21. lemma OAI.WeakMTWTransport.WeakMTW.modified_prefix_weighted_bound line 524
  22. lemma OAI.WeakMTWTransport.WeakMTW.modified_parameter_inequality line 650