OAI/Analysis/DiamondDistortion/RecursiveLenses.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DiamondDistortion.RecursiveApplications.c6 line 17
  2. def OAI.DiamondDistortion.RecursiveApplications.c3 line 18
  3. def OAI.DiamondDistortion.RecursiveApplications.q6 line 20
  4. def OAI.DiamondDistortion.RecursiveApplications.theta line 21
  5. lemma OAI.DiamondDistortion.RecursiveApplications.c6_pos line 23
  6. lemma OAI.DiamondDistortion.RecursiveApplications.c6_le_one line 24
  7. lemma OAI.DiamondDistortion.RecursiveApplications.c3_pos line 31
  8. lemma OAI.DiamondDistortion.RecursiveApplications.c3_le_one line 32
  9. def OAI.DiamondDistortion.RecursiveApplications.PowerInput line 39

    Source documentation

    Polynomial form of the homogeneous power input, used only as an intermediate algebraic rewrite of the displayed sixth and cubic estimates.

    def PowerInput (A : Heads ι X) (n m : ℕ) (c : ℝ) : Prop :=
…
  10. lemma OAI.DiamondDistortion.RecursiveApplications.power_lens line 44
  11. def OAI.DiamondDistortion.RecursiveApplications.SixthInput line 67

    Source documentation

    The exact finite-head sixth input. The S=0 convention is represented by real division, for which the entire right side is zero when S=0.

    def SixthInput (A : Heads ι X) : Prop :=
…
  12. lemma OAI.DiamondDistortion.RecursiveApplications.sixth_to_power line 72
  13. lemma OAI.DiamondDistortion.RecursiveApplications.q6_range line 109
  14. theorem OAI.DiamondDistortion.RecursiveApplications.sixth_lens line 120
  15. theorem OAI.DiamondDistortion.RecursiveApplications.sixth_depth line 126
  16. def OAI.DiamondDistortion.RecursiveApplications.CubicInput line 142

    Source documentation

    Exact finite-head cubic inequality, with its positive radius denominator.

    def CubicInput (A : Heads ι X) : Prop :=
…
  17. lemma OAI.DiamondDistortion.RecursiveApplications.cubic_to_power line 147
  18. lemma OAI.DiamondDistortion.RecursiveApplications.theta_range line 156
  19. theorem OAI.DiamondDistortion.RecursiveApplications.cubic_depth line 173

    Source documentation

    The cubic graph application can also use finite-dimensional paired tails directly; dual separability is unnecessary for this stronger transfer from the same displayed pure-head estimate. The weak-null clause is proved below.

    theorem cubic_depth (A : Heads ι X) (hinput : CubicInput A) {D s : ℝ}
    (k : ℕ) (f : Diamond.Vertex k → X) (hf : Diamond.HasDistortion k f D s) :
    1 ≤ D*(theta D⁻¹)^k := by
…

    Mentions: OAI.DiamondDistortion.RecursiveApplications.CubicInput, OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.HasDistortion, OAI.DiamondDistortion.RecursiveApplications.theta

  20. def OAI.DiamondDistortion.RecursiveApplications.ZeroRootInput line 190
  21. lemma OAI.DiamondDistortion.RecursiveApplications.zero_root_parent line 194
  22. theorem OAI.DiamondDistortion.RecursiveApplications.zero_root_depth line 229