OAI/Analysis/PeriodicLattice/EffectivePotentials.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Effective planar estimates and periodic pressure operators.

  1. theorem OAI.PeriodicLattice.EffectiveFields.bi_diff line 21
  2. theorem OAI.PeriodicLattice.EffectiveFields.bi_estimate line 26
  3. theorem OAI.PeriodicLattice.EffectiveFields.bi_mean line 31
  4. theorem OAI.PeriodicLattice.EffectiveFields.bi_first line 48
  5. theorem OAI.PeriodicLattice.EffectiveFields.bdy_base line 102
  6. theorem OAI.PeriodicLattice.EffectiveFields.pressureSource_base line 105
  7. theorem OAI.PeriodicLattice.EffectiveFields.pressureBase_base line 108
  8. theorem OAI.PeriodicLattice.EffectiveFields.pressureMode_base line 113
  9. def OAI.PeriodicLattice.EffectiveFields.fieldValue line 127
  10. def OAI.PeriodicLattice.EffectiveFields.fieldShift line 129
  11. theorem OAI.PeriodicLattice.EffectiveFields.fieldShift_recursive line 134
  12. def OAI.PeriodicLattice.EffectiveFields.fieldLine line 152
  13. theorem OAI.PeriodicLattice.EffectiveFields.fieldLine_zero line 157
  14. theorem OAI.PeriodicLattice.EffectiveFields.fieldLine_nonneg line 160
  15. theorem OAI.PeriodicLattice.EffectiveFields.fieldShift_value line 163
  16. theorem OAI.PeriodicLattice.EffectiveFields.fieldLine_deriv line 181
  17. theorem OAI.PeriodicLattice.EffectiveFields.field_words line 191
  18. theorem OAI.PeriodicLattice.EffectiveFields.field_diff line 218
  19. def OAI.PeriodicLattice.EffectiveFields.ComponentsEffective line 223
  20. theorem OAI.PeriodicLattice.EffectiveFields.ComponentsEffective.diff line 226
  21. theorem OAI.PeriodicLattice.EffectiveFields.ComponentsEffective.add line 233
  22. theorem OAI.PeriodicLattice.EffectiveFields.ComponentsEffective.sub line 236
  23. theorem OAI.PeriodicLattice.EffectiveFields.ComponentsEffective.scale line 239