WeakLenses.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DiamondDistortion.Midpoint.WeaklyNull line 19
Source documentation
Weak nullity in its exact scalar-functional form, over the real field.
```
def WeaklyNull (z : ℕ → X) : Prop :=
…
```
lemma OAI.DiamondDistortion.Midpoint.finite_dimensional_weak_null line 22
lemma OAI.DiamondDistortion.Midpoint.finite_rank_weak_null line 33
lemma OAI.DiamondDistortion.Midpoint.Heads.weak_pure line 43
lemma OAI.DiamondDistortion.RecursiveApplications.weak_power_lens line 88
theorem OAI.DiamondDistortion.RecursiveApplications.cubic_weak_lens line 109
def OAI.DiamondDistortion.Midpoint.Heads.FiniteVector line 125
Source documentation
Exactly finite-head-supported vectors. For the coordinate models, these are the finite coordinate vectors on the allowed ancestral heads.
```
def Heads.FiniteVector (A : Heads ι X) (x : X) : Prop := ∃ H,A.projection H x=x
```
Mentions: OAI.DiamondDistortion.Midpoint.Heads
def OAI.DiamondDistortion.Midpoint.Heads.Commutes line 128
Source documentation
Coordinate projections commute even when their norms are not uniformly bounded.
```
def Heads.Commutes (A : Heads ι X) : Prop :=
…
```
Mentions: OAI.DiamondDistortion.Midpoint.Heads
lemma OAI.DiamondDistortion.Midpoint.Heads.finite_tail_approx line 131
def OAI.DiamondDistortion.RecursiveApplications.FreeRootInput line 161
def OAI.DiamondDistortion.RecursiveApplications.sumEta line 169
Source documentation
An admissible positive qualitative choice; outside the possible separation range, any number in (0,1) is allowed.
```
def sumEta (γ : ℝ → ℝ → ℝ) (ε : ℝ) : ℝ :=
…
```
lemma OAI.DiamondDistortion.RecursiveApplications.sumEta_range line 172
theorem OAI.DiamondDistortion.RecursiveApplications.free_root_lens line 185
theorem OAI.DiamondDistortion.RecursiveApplications.free_root_depth line 226