OAI/Geometry/RuledCovering/LocalCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RuledApproximation.HasFiniteCover.of_fintype line 12
2. theorem OAI.RuledApproximation.framed_local_cover line 28

   Source documentation

   Convert the finite weighted lattice certificate into actual perpendicular Euclidean cylinders. The factor is the exact area inflation caused by the derivative remainder.

   theorem framed_local_cover (M : Coordinates ≃L[ℝ] Plane) {h L R delta : ℝ}
       (hh : 0 < h) (hL : 0 ≤ L) (hR : 0 ≤ R) (hd : 0 ≤ delta)
       {K U : Set Coordinates} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U)
       (v : Plane → Plane) (A : Coordinates →L[ℝ] Coordinates)
       (hmodel : LatticeModel A L R)
       (hrem : ∀ p ∈ U, ∀ b ∈ U,
         ‖M.symm (v (M p)) - M.symm (v (M b)) - A (p - b)‖ ≤ delta * ‖p - b‖)
       {F : Coordinates → ℝ} (hF : Continuous F) (hFpos : ∀ p, 0 ≤ F p)
       (hFval : ∀ p ∈ U, F p = physicalWeight h (v (M p)))
       {eps : ℝ} (heps : 0 < eps) :
       HasFiniteCover Cylinder.parallelogram (physicalRuled h (M '' K) v L)
         (h * (1 + 2 * L * delta * R) ^ 2 *
   …

   Mentions: OAI.RuledApproximation.Coordinates, OAI.RuledApproximation.Plane, OAI.RuledApproximation.LatticeModel, OAI.RuledApproximation.physicalWeight, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.Cylinder.parallelogram, OAI.RuledApproximation.physicalRuled