OAI/Analysis/Conductivity/Fourier/AnalyticNull.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.measure_inter_zero_of_local line 15
  2. def OAI.ScalarConductivity.AnalyticNullProperty line 28
  3. lemma OAI.ScalarConductivity.analyticNull_real line 33
  4. lemma OAI.ScalarConductivity.analytic_zero_measurable line 47
  5. lemma OAI.ScalarConductivity.analytic_null_rectangle line 57
  6. lemma OAI.ScalarConductivity.analyticNull_prod line 84
  7. lemma OAI.ScalarConductivity.analyticNull_of_equiv line 123
  8. def OAI.ScalarConductivity.splitFinCLE line 142
  9. lemma OAI.ScalarConductivity.splitFinCLE_measurePreserving line 148
  10. theorem OAI.ScalarConductivity.analyticNull_fin line 152
  11. lemma OAI.ScalarConductivity.analytic_zero_volume line 165