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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the geometric derivative budget of the prescribed stages. Local finiteness lets the estimate apply to every derivative of the actual infinite-time field.

  1. theorem OAI.ForcedComputation.ExpandingDetector.half_geometric_sum_le_two line 14
  2. theorem OAI.ForcedComputation.ExpandingDetector.expandingDrift_jet_bound line 23