OAI/Analysis/PeriodicLattice/EffectiveForcing.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Effective periodic velocity, pressure and solenoidal forces.

  1. theorem OAI.PeriodicLattice.EffectiveFields.tensor_base line 21
  2. theorem OAI.PeriodicLattice.EffectiveFields.phase_effective line 36
  3. theorem OAI.PeriodicLattice.EffectiveFields.eta_effective line 40
  4. theorem OAI.PeriodicLattice.EffectiveFields.slope_effective line 44
  5. theorem OAI.PeriodicLattice.EffectiveFields.doubleSlope_effective line 46
  6. theorem OAI.PeriodicLattice.EffectiveFields.velocity_effective line 50
  7. theorem OAI.PeriodicLattice.EffectiveFields.potential_effective line 56
  8. theorem OAI.PeriodicLattice.EffectiveFields.ComponentsEffective.diffusion line 62
  9. theorem OAI.PeriodicLattice.EffectiveFields.ComponentsEffective.transport line 69
  10. theorem OAI.PeriodicLattice.EffectiveFields.ComponentsEffective.gradient line 76
  11. theorem OAI.PeriodicLattice.EffectiveFields.force_effective line 81
  12. theorem OAI.PeriodicLattice.EffectiveFields.solenoidalForce_effective line 85
  13. theorem OAI.PeriodicLattice.CertifiedReal.accuracy_as_inv line 94
  14. theorem OAI.PeriodicLattice.CertifiedReal.accuracy_le_error line 96
  15. theorem OAI.PeriodicLattice.CertifiedReal.computableReal_effective line 101
  16. theorem OAI.PeriodicLattice.EffectiveFields.time_error line 117
  17. theorem OAI.PeriodicLattice.EffectiveFields.field_distance line 127
  18. theorem OAI.PeriodicLattice.EffectiveFields.fieldWord_nearby line 164
  19. theorem OAI.PeriodicLattice.EffectiveFields.word_evaluator line 177
  20. theorem OAI.PeriodicLattice.CertifiedReal.accuracy_pos line 201
  21. theorem OAI.PeriodicLattice.CertifiedReal.accuracy_add line 203
  22. theorem OAI.PeriodicLattice.CertifiedReal.error_pow line 206
  23. theorem OAI.PeriodicLattice.CertifiedReal.accuracy_budget line 212
  24. theorem OAI.PeriodicLattice.CertifiedReal.evaluation_tolerance line 218