OAI/Geometry/QuadricBundles/WeakBaseChange.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.boundedCompositionLp line 20
  2. lemma OAI.QuadricCounterexample.boundedCompositionLp_coe line 25
  3. lemma OAI.QuadricCounterexample.complex_weak_implies_real line 42
  4. lemma OAI.QuadricCounterexample.real_weakLimit_map line 49
  5. lemma OAI.QuadricCounterexample.real_weakLimit_approximate_graph line 55
  6. lemma OAI.QuadricCounterexample.map_restrict_involution_le line 76
  7. lemma OAI.QuadricCounterexample.boundedMultiplier_memLp line 120
  8. def OAI.QuadricCounterexample.boundedMultiplierLp line 130
  9. lemma OAI.QuadricCounterexample.boundedMultiplierLp_coe line 158
  10. lemma OAI.QuadricCounterexample.compact_involution_map_bound line 170
  11. abbrev OAI.QuadricCounterexample.MatrixCoefficients line 198
  12. lemma OAI.QuadricCounterexample.matrix_eq_of_quadratic_eq line 200
  13. def OAI.QuadricCounterexample.congruenceCoefficients line 206
  14. lemma OAI.QuadricCounterexample.congruenceCoefficients_apply line 212
  15. lemma OAI.QuadricCounterexample.continuous_congruenceCoefficients line 215
  16. lemma OAI.QuadricCounterexample.TwistedPshForm.matrix_compatible line 222
  17. lemma OAI.QuadricCounterexample.coordinateChange_symm line 235
  18. lemma OAI.QuadricCounterexample.coordinateChange_involutive line 239
  19. lemma OAI.QuadricCounterexample.coordinateChange_measurable line 244
  20. lemma OAI.QuadricCounterexample.coordinateChange_contDiffOn line 248
  21. lemma OAI.QuadricCounterexample.coordinateChange_mapsTo_overlap line 262
  22. lemma OAI.QuadricCounterexample.coordinateChange_compact_bound line 278
  23. lemma OAI.QuadricCounterexample.L2_norm_tendsto_zero_of_bounded_ae line 294
  24. lemma OAI.QuadricCounterexample.real_weakLimit_two_maps line 323