OAI/Analysis/DiamondDistortion/PathLenses.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DiamondDistortion.PathApplications.FlowInput line 18

    Source documentation

    The positive-flow and trimming inputs, with their distinct coefficient B.

    def FlowInput (A : Heads ι X) (B : ℝ) : Prop :=
…
  2. lemma OAI.DiamondDistortion.PathApplications.flow_square line 22
  3. lemma OAI.DiamondDistortion.PathApplications.square_depth line 33
  4. def OAI.DiamondDistortion.PathApplications.linearC line 39
  5. lemma OAI.DiamondDistortion.PathApplications.linearC_pos line 40
  6. theorem OAI.DiamondDistortion.PathApplications.linear_flow line 42
  7. theorem OAI.DiamondDistortion.PathApplications.linear_trimming line 53
  8. def OAI.DiamondDistortion.PathApplications.ArbitraryTailInput line 61

    Source documentation

    Exact arbitrary-displacement cancellation input (unlike a pure-tail assertion).

    def ArbitraryTailInput (A : Heads ι X) (C : ℝ) : Prop :=
…
  9. lemma OAI.DiamondDistortion.PathApplications.arbitrary_tail_square line 65
  10. theorem OAI.DiamondDistortion.PathApplications.quadratic_cost line 77
  11. def OAI.DiamondDistortion.PathApplications.StoppedInput line 85

    Source documentation

    The independent stopped-flow intrinsic input, with no change to its energy average.

    def StoppedInput (A : Heads ι X) : Prop :=
…
  12. theorem OAI.DiamondDistortion.PathApplications.stopped_flow line 89
  13. def OAI.DiamondDistortion.PathApplications.StartInput line 101
  14. lemma OAI.DiamondDistortion.PathApplications.start_square line 105
  15. theorem OAI.DiamondDistortion.PathApplications.start_cost line 111
  16. def OAI.DiamondDistortion.PathApplications.clippingC line 118
  17. def OAI.DiamondDistortion.PathApplications.clippingQ line 119
  18. def OAI.DiamondDistortion.PathApplications.clippingGamma line 120
  19. lemma OAI.DiamondDistortion.PathApplications.clipping_bounds line 122
  20. lemma OAI.DiamondDistortion.PathApplications.clipping_actual_child line 138

    Source documentation

    Actual-child selection at the clipping half-gain. No infinite supremum is attained.

    lemma clipping_actual_child (A : Heads ι X) (hinput : A.ParametricInput (1/2) 4)
    {D : ℝ} (hD : 1 ≤ D) {x : X} (z : ℕ → X) (hxD : ‖x‖ ≤ D)
    (hs : ∀ i j,i ≠ j → 2 ≤ ‖z i-z j‖) :
    ∃ i,‖x‖+clippingGamma D/(2*clippingQ D) < max ‖x+z i‖ ‖x-z i‖ := by
…

    Mentions: OAI.DiamondDistortion.PathApplications.clippingGamma, OAI.DiamondDistortion.PathApplications.clippingQ

  21. theorem OAI.DiamondDistortion.PathApplications.linear_clipping line 156
  22. lemma OAI.DiamondDistortion.PathApplications.unit_from_square line 178
  23. theorem OAI.DiamondDistortion.PathApplications.tail_seven line 185
  24. theorem OAI.DiamondDistortion.PathApplications.tail_pruning line 203

    Source documentation

    The pruning parameter is not optimized or silently replaced by the 7-bound.

    theorem tail_pruning (A : Heads ι X) (hinput : ArbitraryTailInput A 9)
    {D s γ : ℝ} (hγ : 0 < γ) (hγ2 : γ < 1/2)
    (hparameter : 9*Real.sqrt ((1+γ)^2-(1-2*γ)^2) < 2*D⁻¹/3)
    (k : ℕ) (f : Diamond.Vertex k → X) (hf : Diamond.HasDistortion k f D s) :
    D⁻¹ ≤ (1-γ)^k := by
…

    Mentions: OAI.DiamondDistortion.PathApplications.ArbitraryTailInput, OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.HasDistortion

  25. def OAI.DiamondDistortion.PathApplications.incomparableK line 223
  26. lemma OAI.DiamondDistortion.PathApplications.incomparableK_gt_one line 224
  27. theorem OAI.DiamondDistortion.PathApplications.incomparable_segments line 231
  28. def OAI.DiamondDistortion.PathApplications.ComponentSumInput line 254

    Source documentation

    Component-to-sum finite-codimensional input, exactly at arbitrary unit centers.

    def ComponentSumInput (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X] : Prop :=
…
  29. theorem OAI.DiamondDistortion.PathApplications.component_sum line 259