Phase.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.ray_channel line 20
Source documentation
channel perturbation estimate.
```
private lemma ray_channel (A : Form M) (f : Grid M → ℂ) (x : Grid M) :
    (channel A x).Cx f = (label A).Cx fun z => f (x+z) := by
…
```
Mentions: OAI.FourierLLogL.Dyadic.Grid
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.duet_decode line 28
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.gain_decode line 48
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.energy_near_channel line 55
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.near_size line 110
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.node_compress line 126
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.halo_limit line 129
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.channel_inner line 138
Source documentation
Combining errors after activation. First main interval may use b=1, then inner always.
```
lemma channel_inner :
    ∀ᶠ j : ℕ in atTop, ∀ (i : ℕ), i ≤ mainIx j → ∀ (M : ℕ)
    (p q : Scene M), q.here.below p.here → dye q=dye p → Climb q →
    ∀ u v k : Grid M, delta (dye p) k ≤ sepRad j →
      rad (u-v-k) ≤ 2*spotLimit p j i true →
        (0 < i → ¬ snag ⟨true,i-1⟩ u (⟨q,q,false⟩:Beat M)) →
        Run.Streak.innerV (rose ⟨true,i⟩ v) q := by
…
```
Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Paths.dye, OAI.FourierLLogL.Dyadic.Procedure.Paths.Climb, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.rad, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.snag, OAI.FourierLLogL.Dyadic.Procedure.Paths.Run.Streak.innerV, OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.rose
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.gain_point line 184
lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scalar_energy line 198
Source documentation
big unlabelled coefficients force labelled high
```
lemma scalar_energy (s : Scene M) (h : Fit s) (u) :
    ‖scalar s u‖^2 ≤ 4*energy s u := by
…
```
Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene, OAI.FourierLLogL.Dyadic.Procedure.Paths.Fit