OAI/Geometry/RuledCovering/HyperbolicCover.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RuledApproximation.sumDifference line 13

   Source documentation

   Sum-and-difference coordinates conjugate a hyperbolic derivative to the square lattice template.

   def sumDifference : Coordinates ≃ₗ[ℝ] Coordinates where
   …

   Mentions: OAI.RuledApproximation.Coordinates

2. lemma OAI.RuledApproximation.hyperbolic_frame line 21
3. lemma OAI.RuledApproximation.HasFiniteCover.mono line 52
4. lemma OAI.RuledApproximation.HasFiniteCover.empty line 58
5. lemma OAI.RuledApproximation.HasFiniteCover.union line 63
6. lemma OAI.RuledApproximation.physicalRuled_union line 80
7. lemma OAI.RuledApproximation.physicalRuled_mono line 86
8. lemma OAI.RuledApproximation.physicalRuled_empty line 91
9. lemma OAI.RuledApproximation.compact_cut_integral line 96

   Source documentation

   Compact pieces cut along a null frontier have exactly additive cost, even when the original compact set itself has a positive-area frontier.

   lemma compact_cut_integral {K O : Set Plane} (hK : IsCompact K) (hO : IsOpen O)
       (hnull : volume (frontier O) = 0) {F : Plane → ℝ} (hF : IntegrableOn F K) :
       IsCompact (K ∩ closure O) ∧ IsCompact (K \ O) ∧
       K = (K ∩ closure O) ∪ (K \ O) ∧
       (∫ x in K, F x) = (∫ x in K ∩ closure O, F x) + (∫ x in K \ O, F x) := by
   …

   Mentions: OAI.RuledApproximation.Plane

10. theorem OAI.RuledApproximation.glue_finite_local_covers line 126

    Source documentation

    Finite gluing over regular open patches. Only the patch frontiers must be null; there is deliberately no restriction on the label set's own frontier.

    theorem glue_finite_local_covers {shape : Cylinder → Prop} (h L : ℝ) (v : Plane → Plane)
        (F : Plane → ℝ) {A : ℝ}
        {ι : Type*} (s : Finset ι) (O U : ι → Set Plane)
        (hO : ∀ i ∈ s, IsOpen (O i)) (hOU : ∀ i ∈ s, closure (O i) ⊆ U i)
        (hnull : ∀ i ∈ s, volume (frontier (O i)) = 0)
        (hlocal : ∀ i ∈ s, ∀ Q : Set Plane, IsCompact Q → Q ⊆ U i →
          ∀ eps : ℝ, 0 < eps → HasFiniteCover shape (physicalRuled h Q v L)
            (A * (∫ p in Q, F p) + eps))
        {K : Set Plane} (hK : IsCompact K) (hF : IntegrableOn F K)
        (hcover : K ⊆ ⋃ i ∈ s, O i) {eps : ℝ} (heps : 0 < eps) :
        HasFiniteCover shape (physicalRuled h K v L) (A * (∫ p in K, F p) + eps) := by
    …

    Mentions: OAI.RuledApproximation.Cylinder, OAI.RuledApproximation.Plane, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.physicalRuled

11. lemma OAI.RuledApproximation.physicalWeight_pos line 164
12. lemma OAI.RuledApproximation.physicalWeight_continuous line 169
13. lemma OAI.RuledApproximation.exists_small_inflation line 176
14. theorem OAI.RuledApproximation.hyperbolic_local_patch line 188

    Source documentation

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

    theorem hyperbolic_local_patch {h L B : ℝ} (hh : 0 < h) (hL : 0 < L) (hB : 1 < B)
        {v : Plane → Plane} {U : Set Plane} (hU : IsOpen U) (hv : ContDiffOn ℝ 1 v U)
        {p : Plane} (hp : p ∈ U) (hhyp : HyperbolicAt L v p) :
        ∃ V : Set Plane, IsOpen V ∧ p ∈ V ∧ ∀ K : Set Plane, IsCompact K → K ⊆ V →
          ∀ eps : ℝ, 0 < eps → HasFiniteCover Cylinder.parallelogram (physicalRuled h K v L)
            (h * B * (∫ q in K, physicalWeight h (v q)) + eps) := by
    …

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

15. theorem OAI.RuledApproximation.globalize_local_covers line 254

    Source documentation

    Compactness and null-frontier patches globalize the finite local producer.

    theorem globalize_local_covers {shape : Cylinder → Prop} (h L : ℝ) (v : Plane → Plane)
        (F : Plane → ℝ) (A : ℝ) {K : Set Plane} (hK : IsCompact K) (hF : IntegrableOn F K)
        (hpatch : ∀ p ∈ K, ∃ V : Set Plane, IsOpen V ∧ p ∈ V ∧
          ∀ Q : Set Plane, IsCompact Q → Q ⊆ V → ∀ eps : ℝ, 0 < eps →
          HasFiniteCover shape (physicalRuled h Q v L) (A * (∫ q in Q, F q) + eps))
        {eps : ℝ} (heps : 0 < eps) :
        HasFiniteCover shape (physicalRuled h K v L) (A * (∫ q in K, F q) + eps) := by
    …

    Mentions: OAI.RuledApproximation.Cylinder, OAI.RuledApproximation.Plane, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.physicalRuled

16. lemma OAI.RuledApproximation.exists_inflation_budget line 280
17. theorem OAI.RuledApproximation.physical_hyperbolic_cover line 291

    Source documentation

    General physical weighted hyperbolic approximation, before isometry transport.

    theorem physical_hyperbolic_cover {h L : ℝ} {D : Set Plane} {v : Plane → Plane}
        (hh : 0 < h) (hL : 0 < L) (hD : IsCompact D) (hv : SmoothNear 1 D v)
        (hhyp : ∀ p ∈ D, HyperbolicAt L v p) {eps : ℝ} (heps : 0 < eps) :
        HasFiniteCover Cylinder.parallelogram (physicalRuled h D v L)
          (h * (∫ p in D, physicalWeight h (v p)) + eps) := by
    …

    Mentions: OAI.RuledApproximation.Plane, OAI.RuledApproximation.SmoothNear, OAI.RuledApproximation.HyperbolicAt, OAI.RuledApproximation.HasFiniteCover, OAI.RuledApproximation.Cylinder.parallelogram, OAI.RuledApproximation.physicalRuled, OAI.RuledApproximation.physicalWeight