OAI/Analysis/Conductivity/Fourier/PoissonTraceRate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.poissonMultiplier_sub_one_bound line 15
  2. lemma OAI.ScalarConductivity.torusPoissonFlow_trace_rate line 21
  3. lemma OAI.ScalarConductivity.torusRate_sq_polynomial_bound line 39
  4. lemma OAI.ScalarConductivity.sourceAngularTrace_H1_summable line 65
  5. lemma OAI.ScalarConductivity.sourceAngularTrace_rate_sq_summable line 87
  6. lemma OAI.ScalarConductivity.centralTrace_rate_sq_summable line 98
  7. lemma OAI.ScalarConductivity.centralTrace_rate_memℓp line 111
  8. lemma OAI.ScalarConductivity.complexL2_norm_sq line 126
  9. lemma OAI.ScalarConductivity.continuousMap_L2_sq line 131
  10. lemma OAI.ScalarConductivity.torusPoissonContinuous_trace_sq line 138
  11. lemma OAI.ScalarConductivity.endPoissonField_trace_sq line 150