Transfers.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DiamondDistortion.Diamond.quotient_full_gain line 18
theorem OAI.DiamondDistortion.Diamond.quotient_transfer line 40
def OAI.DiamondDistortion.Diamond.StableParent line 52
Source documentation
A parent at any of the k replacement stages, with all of its actual children bounded by the specified multiple of its own slope. The recursion restricts to old vertices and therefore includes every stage, not just the last one.
```
def StableParent (c : ℝ) : (k : ℕ) → (Vertex k → X) → Prop
  | 0,_ => False
  | n+1,f => (∃ e : Edge n,∀ (i : ℕ) (b : Bool),
      ‖slope f (e,i,b)‖ ≤ c*‖slope (fun v => f (Sum.inl v)) e‖) ∨
      StableParent c n (fun v => f (Sum.inl v))
```
Mentions: OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.Edge, OAI.DiamondDistortion.Diamond.slope
lemma OAI.DiamondDistortion.Diamond.absence_stable_growth line 58
theorem OAI.DiamondDistortion.Diamond.stable_parent line 78
def OAI.DiamondDistortion.Diamond.EnlargedLensExcluded line 91
Source documentation
Exact exclusion of infinite separated families in every enlarged unit-center lens, retaining the radius and separation as independent parameters.
```
def EnlargedLensExcluded (X : Type*) [NormedAddCommGroup X] (R β : ℝ) : Prop :=
…
```
lemma OAI.DiamondDistortion.Diamond.enlarged_parent line 96
theorem OAI.DiamondDistortion.Diamond.enlarged_backward line 129
theorem OAI.DiamondDistortion.Diamond.stable_parent_obstruction line 150
def OAI.DiamondDistortion.Diamond.stageSup line 161
Source documentation
Supremum of all edge slopes at one stage; not a maximum.
```
def stageSup {k : ℕ} (f : Vertex k → X) : ℝ :=
…
```
Mentions: OAI.DiamondDistortion.Diamond.Vertex
lemma OAI.DiamondDistortion.Diamond.slope_le_stageSup line 164
lemma OAI.DiamondDistortion.Diamond.stageSup_le line 168
lemma OAI.DiamondDistortion.Diamond.parametric_Q_one line 176
theorem OAI.DiamondDistortion.Diamond.parametric_stage line 180

theorem OAI.DiamondDistortion.Diamond.parametric line 212

Source documentation

The exact parameterized graph depth conclusion; no optimization performed.

theorem parametric (A : Midpoint.Heads ι X) {a b lam D s : ℝ}
    (ha : 0 < a) (hb : 0 < b) (hlam : 0 < lam) (hinput : A.ParametricInput a b)
    (hΔ : 0 < a*lam-(Real.sqrt (1+b*lam^2)-1)*D)
    (k : ℕ) (f : Vertex k → X) (hf : HasDistortion k f D s) :
    1+(k:ℝ)*(a*lam-(Real.sqrt (1+b*lam^2)-1)*D) ≤ D := by
…

Mentions: OAI.DiamondDistortion.Midpoint.Heads, OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.HasDistortion

theorem OAI.DiamondDistortion.Diamond.parametric_twentyfour line 234