OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/PeriodicLatticeTransform.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A rational transverse transformation of the periodic lattice field. The first direction is ignorable for this field, so its velocity can be scaled without defining a nonintegral dilation of the circle.

  1. theorem OAI.PeriodicLattice.RapidTorus.realRingHomCompTriple line 15
  2. theorem OAI.PeriodicLattice.RapidTorus.spaceContinuousSMul line 18
  3. def OAI.PeriodicLattice.RapidTorus.transverseLinear line 20
  4. theorem OAI.PeriodicLattice.RapidTorus.transverseLinear_apply line 30
  5. theorem OAI.PeriodicLattice.RapidTorus.transverseLinear_bound line 39
  6. def OAI.PeriodicLattice.RapidTorus.shiftVector line 51
  7. def OAI.PeriodicLattice.RapidTorus.shift line 55
  8. def OAI.PeriodicLattice.RapidTorus.shiftedField line 57
  9. def OAI.PeriodicLattice.RapidTorus.transformedField line 58
  10. theorem OAI.PeriodicLattice.RapidTorus.shiftedField_smooth line 61
  11. theorem OAI.PeriodicLattice.RapidTorus.transformedField_smooth line 69
  12. theorem OAI.PeriodicLattice.RapidTorus.shiftedField_spaceD line 73
  13. theorem OAI.PeriodicLattice.RapidTorus.transformedField_spaceD line 88
  14. theorem OAI.PeriodicLattice.RapidTorus.transformedField_fullTimeD line 99
  15. theorem OAI.PeriodicLattice.RapidTorus.transformedField_coordD line 107
  16. theorem OAI.PeriodicLattice.RapidTorus.transformedField_word line 114
  17. theorem OAI.PeriodicLattice.RapidTorus.transformedField_meanZero line 123