OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/SmallComplexPower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform cancellation for bounded complex powers near one

  1. theorem OAI.DefocusingNLS.norm_log_mul_le_one_of_small line 10
  2. theorem OAI.DefocusingNLS.norm_cpow_sub_one_le_of_small line 25
  3. theorem OAI.DefocusingNLS.norm_log_mul_cpow_le_of_small line 44