OAI/Analysis/FreeWords/VariableUltraFactor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKVariableUltra.gns_factor_of_center_scalar line 21
  2. theorem OAI.KKVariableUltra.map_commutator_zero line 51
  3. theorem OAI.KKVariableUltra.gns_commutator_norm_zero line 56
  4. theorem OAI.KKVariableUltra.map_eq_scalar_of_centered_zero line 64
  5. theorem OAI.KKVariableUltra.gns_center_scalar_of_commutator_norm line 70
  6. theorem OAI.KKVariableUltra.coordinate_gns_zero_of_norm_tendsto line 83
  7. theorem OAI.KKVariableUltra.coordinate_centered_norm_tendsto_zero line 92
  8. theorem OAI.KKVariableUltra.coordinate_commutator_bound line 120
  9. theorem OAI.KKVariableUltra.coordinate_center_scalar line 132
  10. theorem OAI.KKVariableUltra.coordinate_factor line 153