OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingCenterSize.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform address dependence of the center jets. Only a linear factor in the largest address remains after differentiating the constant positions.

  1. theorem OAI.ForcedComputation.ExpandingDetector.schedule_coefficient_bounds line 13
  2. theorem OAI.ForcedComputation.ExpandingDetector.scheduledCenter_coordinate_jet_bound line 41