OAI/Analysis/CircleDomains/Selection/ContinuousRunningMaximum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A continuous running maximum for nonnegative continuous functions. Using the norm of a curried map avoids any selection of maximizers.

  1. def OAI.CircleDomainRigidity.runningMaximum line 14
  2. lemma OAI.CircleDomainRigidity.runningMaximum_nonneg line 19
  3. lemma OAI.CircleDomainRigidity.le_runningMaximum line 24
  4. lemma OAI.CircleDomainRigidity.runningMaximum_le line 33
  5. lemma OAI.CircleDomainRigidity.runningMaximum_mono line 42
  6. lemma OAI.CircleDomainRigidity.runningMaximum_eq_of_constant line 48