OAI/Geometry/QuadricBundles/TraceMetrics.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.standardChartIndex line 14
  2. lemma OAI.QuadricCounterexample.standardChartIndex_lt line 15
  3. lemma OAI.QuadricCounterexample.standardChartNat_index line 17
  4. lemma OAI.QuadricCounterexample.EqualizerData.twist_coordinateDomain line 20
  5. lemma OAI.QuadricCounterexample.EqualizerData.twist_chart line 27
  6. lemma OAI.QuadricCounterexample.EqualizerData.twist_domain line 32
  7. lemma OAI.QuadricCounterexample.SmoothHermitianMetric.chart_psh line 39
  8. lemma OAI.QuadricCounterexample.continuous_matrix_of_quadratic line 53
  9. def OAI.QuadricCounterexample.matrixRootTrace line 75
  10. lemma OAI.QuadricCounterexample.matrixRootTrace_quadratic line 79
  11. lemma OAI.QuadricCounterexample.matrixRootTrace_posDef line 90
  12. lemma OAI.QuadricCounterexample.continuous_matrixRootTrace line 99
  13. lemma OAI.QuadricCounterexample.matrixRootTrace_psh line 120
  14. lemma OAI.QuadricCounterexample.matrixRootTrace_anyRoot line 142
  15. lemma OAI.QuadricCounterexample.root_pow line 161
  16. lemma OAI.QuadricCounterexample.root_norm line 164
  17. def OAI.QuadricCounterexample.rootSwitchEquiv line 167
  18. lemma OAI.QuadricCounterexample.scalarCoordinateChange_root line 171
  19. lemma OAI.QuadricCounterexample.coordinateChange_pow line 178
  20. lemma OAI.QuadricCounterexample.coordinateOverlap_pow line 183
  21. lemma OAI.QuadricCounterexample.polarizationTransition_affine line 187
  22. lemma OAI.QuadricCounterexample.polarizationTransition_root_norm line 192
  23. lemma OAI.QuadricCounterexample.matrixRootTrace_change line 199
  24. lemma OAI.QuadricCounterexample.quadraticValue_congruence line 214
  25. lemma OAI.QuadricCounterexample.quadraticValue_scalar line 218
  26. lemma OAI.QuadricCounterexample.quadraticValue_sum_smul line 225
  27. lemma OAI.QuadricCounterexample.SmoothHermitianMetric.twist_quadratic_change line 234
  28. lemma OAI.QuadricCounterexample.SmoothHermitianMetric.trace_quadratic_change line 255
  29. lemma OAI.QuadricCounterexample.polarizationTransition_power line 281
  30. def OAI.QuadricCounterexample.traceScalar line 287
  31. lemma OAI.QuadricCounterexample.traceScalar_power line 290
  32. lemma OAI.QuadricCounterexample.SmoothHermitianMetric.trace_change line 298
  33. structure OAI.QuadricCounterexample.TwistedPshForm line 322
  34. def OAI.QuadricCounterexample.TwistedPshForm.value line 335
  35. lemma OAI.QuadricCounterexample.TwistedPshForm.value_continuous line 338
  36. lemma OAI.QuadricCounterexample.TwistedPshForm.value_nonneg line 343
  37. lemma OAI.QuadricCounterexample.TwistedPshForm.value_scalar line 347
  38. def OAI.QuadricCounterexample.TwistedPshForm.rescale line 351
  39. lemma OAI.QuadricCounterexample.TwistedPshForm.value_rescale line 372
  40. lemma OAI.QuadricCounterexample.TwistedPshForm.quadratic_bound_of_unit_ball line 378
  41. lemma OAI.QuadricCounterexample.TwistedPshForm.exists_normalized line 402
  42. def OAI.QuadricCounterexample.SmoothHermitianMetric.tracedForm line 440
  43. lemma OAI.QuadricCounterexample.norm_transpose_mulVec_le line 464
  44. lemma OAI.QuadricCounterexample.traceScalar_le line 479
  45. lemma OAI.QuadricCounterexample.EqualizerData.coordinateTransition_continuousOn line 491
  46. def OAI.QuadricCounterexample.switchRegion line 498
  47. lemma OAI.QuadricCounterexample.switchRegion_compact line 501
  48. lemma OAI.QuadricCounterexample.switchRegion_subset line 516
  49. lemma OAI.QuadricCounterexample.exists_unit_coordinateChange line 523
  50. lemma OAI.QuadricCounterexample.TwistedPshForm.local_bound line 538
  51. lemma OAI.QuadricCounterexample.norm_matrix_of_quadratic_bound line 586
  52. lemma OAI.QuadricCounterexample.norm_coefficients_of_quadratic_bound line 618