RegularFiberDomain.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.regularPositiveFiberDomain line 18
Source documentation
The largest open positive base domain on which the literal transverse fibers are compact and contain zero in their interiors. It is defined directly from the convex body's fibers, without any estimate or derivative hypothesis.
```
def regularPositiveFiberDomain {k m : ℕ} (C : Set (Space k × Space m)) : Set (Space k) :=
…
```
Mentions: OAI.AffineBernstein.Space
lemma OAI.AffineBernstein.regularPositiveFiberDomain_isOpen line 22
lemma OAI.AffineBernstein.regularPositiveFiberDomain_positive line 30
lemma OAI.AffineBernstein.regularPositiveFiberDomain_compact line 35
lemma OAI.AffineBernstein.regularPositiveFiberDomain_zero line 40
lemma OAI.AffineBernstein.openBox_subset_regularPositiveFiberDomain line 46
def OAI.AffineBernstein.logarithmicBox line 65
Source documentation
Closed logarithmic boxes agree exactly with the source definition.
```
def logarithmicBox (k : ℕ) (L : ℝ) : Set (Space k) := {x | ∀ i, |x i| ≤ L}
```
Mentions: OAI.AffineBernstein.Space

theorem OAI.AffineBernstein.LocalDistanceConverges.eventually_regular_logBox line 69

Source documentation

Every fixed logarithmic box is eventually available in a normalized-model approximation. The regular domains are produced from the actual fibers.

theorem LocalDistanceConverges.eventually_regular_logBox
    {k m : ℕ} {Cj : ℕ → Set (Space k × Space m)} {C : Set (Space k × Space m)}
    (h : LocalDistanceConverges Cj C) (hC : IsModelShape C)
    (hclj : ∀ j, IsClosed (Cj j)) (hcvj : ∀ j, Convex ℝ (Cj j))
    (hnej : ∀ j, (Cj j).Nonempty) {r R : ℝ} (hr : 0 < r)
    (hin : closedBall (0 : Space m) r ⊆
      modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))))
    (hout : modelFiber C (WithLp.toLp 2 (fun _ : Fin k => (1:ℝ))) ⊆ closedBall 0 R)
    (T : ℕ) : ∀ᶠ j in atTop,
      logarithmicBox k T ⊆ logSpace '' regularPositiveFiberDomain (Cj j) := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.LocalDistanceConverges, OAI.AffineBernstein.IsModelShape, OAI.AffineBernstein.modelFiber, OAI.AffineBernstein.logarithmicBox, OAI.AffineBernstein.logSpace, OAI.AffineBernstein.regularPositiveFiberDomain