SquareCover.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RuledApproximation.framed_local_cover_of_shape line 14

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_of_shape (M : Coordinates ≃L[ℝ] Plane) {h L R delta : ℝ}
    (shape : Cylinder → Prop)
    (hshape : ∀ b : Coordinates, ∀ a : ℝ, 0 < a → ∀ g : Plane,
      shape (projectedCylinder h g (M '' closedBall b a)))
    (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)))
…

Mentions: OAI.RuledApproximation.Coordinates, OAI.RuledApproximation.Plane, OAI.RuledApproximation.Cylinder, OAI.RuledApproximation.projectedCylinder, OAI.RuledApproximation.LatticeModel, OAI.RuledApproximation.physicalWeight

theorem OAI.RuledApproximation.nilpotent_local_patch line 88

Source documentation

Every square-zero label has a patch whose compact subsets admit finite covers, with one prescribed arbitrarily small area inflation.

theorem nilpotent_local_patch {h B : ℝ} (hh : 0 < h) (hB : 1 < B)
    {v : Plane → Plane} {U : Set Plane} (hU : IsOpen U) (hv : ContDiffOn ℝ 1 v U)
    {p : Plane} (hp : p ∈ U) (hnil : (fderiv ℝ v p).comp (fderiv ℝ v p) = 0) :
    ∃ V : Set Plane, IsOpen V ∧ p ∈ V ∧ ∀ K : Set Plane, IsCompact K → K ⊆ V →
      ∀ eps : ℝ, 0 < eps → HasFiniteCover (squareProjected h) (physicalRuled h K v 1)
        (h * B * (∫ q in K, physicalWeight h (v q)) + eps) := by
…

Mentions: OAI.RuledApproximation.Plane, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.squareProjected, OAI.RuledApproximation.physicalRuled, OAI.RuledApproximation.physicalWeight

theorem OAI.RuledApproximation.nilpotent_physical_cover line 159
Source documentation
Finite square-tile approximation, with unrestricted local shear and arbitrary compact labels.
```
theorem nilpotent_physical_cover {h : ℝ} {D : Set Plane} {v : Plane → Plane}
    (hh : 0 < h) (hD : IsCompact D) (hv : SmoothNear 1 D v)
    (hnil : ∀ p ∈ D, (fderiv ℝ v p).comp (fderiv ℝ v p) = 0)
    {eps : ℝ} (heps : 0 < eps) :
    HasFiniteCover (squareProjected h) (physicalRuled h D v 1)
      (h * (∫ p in D, physicalWeight h (v p)) + eps) := by
…
```
Mentions: OAI.RuledApproximation.Plane, OAI.RuledApproximation.SmoothNear, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.squareProjected, OAI.RuledApproximation.physicalRuled, OAI.RuledApproximation.physicalWeight
lemma OAI.RuledApproximation.unitSquare_parallelogram line 175
lemma OAI.RuledApproximation.IsSquareTile.parallelogram line 192