OAI/Analysis/IntegralMeans/TraceIdentity.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.pairLaplacian line 24
  2. def OAI.Brennan.traceFluxX line 27
  3. def OAI.Brennan.traceFluxY line 30
  4. lemma OAI.Brennan.traceFlux_contDiffAt line 33
  5. lemma OAI.Brennan.divergence_traceFlux line 42
  6. lemma OAI.Brennan.continuousAt_pairLaplacian line 60
  7. lemma OAI.Brennan.rectangle_trace_identity line 68
  8. lemma OAI.Brennan.half_trace_rectangle line 125
  9. lemma OAI.Brennan.ofReal_integral_le_lintegral_abs line 185
  10. lemma OAI.Brennan.half_trace_lintegral_le line 191
  11. def OAI.Brennan.secondReal line 217
  12. def OAI.Brennan.complexSecondReal line 219
  13. lemma OAI.Brennan.secondReal_comp line 221
  14. lemma OAI.Brennan.bilinear_complex_rotation line 238
  15. lemma OAI.Brennan.laplacian_eq_secondReal line 251
  16. lemma OAI.Brennan.laplacian_eq_complexSecondReal line 255
  17. lemma OAI.Brennan.fderiv_real_complex_apply line 259
  18. lemma OAI.Brennan.laplacian_holomorphic_comp line 264
  19. lemma OAI.Brennan.pairLaplacian_complex line 281
  20. lemma OAI.Brennan.laplacian_eq_zero_outside_tsupport line 298
  21. lemma OAI.Brennan.continuous_laplacian line 307
  22. lemma OAI.Brennan.compactSupport_laplacian line 318
  23. lemma OAI.Brennan.conformal_lintegral_le line 325
  24. lemma OAI.Brennan.conformal_cutoff_trace_bound line 343
  25. lemma OAI.Brennan.exists_trace_smooth_cutoff line 408
  26. lemma OAI.Brennan.conformal_trace_bound line 417
  27. lemma OAI.Brennan.class_trace_bound line 453
  28. lemma OAI.Brennan.uniform_relative_class_bound line 465