OAI/Analysis/DiamondDistortion/StartModels.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DiamondDistortion.StartModel.RealNormed line 20

    Source documentation

    A local bundle used only to recurse over the finite tree height.

    structure RealNormed where
…
  2. instance OAI.DiamondDistortion.StartModel.(instance at line 25) line 25
  3. abbrev OAI.DiamondDistortion.StartModel.representationModel line 30

    Source documentation

    At each node the root-start coefficients form ℓ¹ over the possible endpoints; the children form ℓ² of their own representation spaces. The outer ℓ¹ pair is exactly q_s=m_s+(Σ q_c²)^(1/2).

    abbrev representationModel : ℕ → RealNormed
  | 0 => ⟨ℝ⟩
  | h+1 =>
      let M := representationModel h
…

    Mentions: OAI.DiamondDistortion.StartModel.RealNormed

  4. abbrev OAI.DiamondDistortion.StartModel.Rep line 35
  5. def OAI.DiamondDistortion.StartModel.output line 39

    Source documentation

    Coordinate output, including the absolutely summable root-start paths and the child contribution. No finite-support restriction is made on a Rep.

    def output : (h : ℕ) → (Rep h →ₗ[ℝ] (Coord h → ℝ))
  | 0 => {
      toFun a := fun _ => a
…

    Mentions: OAI.DiamondDistortion.StartModel.Rep

  6. lemma OAI.DiamondDistortion.StartModel.output_coordinate line 59
  7. abbrev OAI.DiamondDistortion.StartModel.atom line 75

    Source documentation

    Singleton segments, used only as a right inverse, not as a restriction on the allowed representations.

    abbrev atom : (h : ℕ) → Coord h → (ℝ →ₗ[ℝ] Rep h)
  | 0,_ => LinearMap.id
  | h+1,.inl _ =>
    (WithLp.linearEquiv 1 ℝ (L1 (h+1) × lp (fun _ : ℕ => Rep h) 2)).symm.toLinearMap.comp
      ((lp.lsingle (𝕜 := ℝ) (E := fun _ : Coord (h+1) => ℝ) 1 (root (h+1))).prod 0)
…

    Mentions: OAI.DiamondDistortion.StartModel.Rep

  8. lemma OAI.DiamondDistortion.StartModel.output_atom line 84
  9. def OAI.DiamondDistortion.StartModel.finiteSection line 126

    Source documentation

    The infimum over the full nested ℓ¹/ℓ² representation space.

    def finiteSection (h : ℕ) : Vec h →ₗ[ℝ] Rep h := Finsupp.lsum ℝ (atom h)

    Mentions: OAI.DiamondDistortion.StartModel.Rep, OAI.DiamondDistortion.StartModel.atom

  10. def OAI.DiamondDistortion.StartModel.relation line 128
  11. def OAI.DiamondDistortion.StartModel.finiteCost line 145
  12. lemma OAI.DiamondDistortion.StartModel.finiteCost_eq_sInf line 146
  13. lemma OAI.DiamondDistortion.StartModel.coordinate_le_cost line 149
  14. def OAI.DiamondDistortion.StartModel.forestSeminorm line 156
  15. lemma OAI.DiamondDistortion.StartModel.forest_coordinate line 157
  16. def OAI.DiamondDistortion.StartModel.data line 165
  17. abbrev OAI.DiamondDistortion.StartModel.Space line 168
  18. def OAI.DiamondDistortion.StartModel.heads line 169
  19. theorem OAI.DiamondDistortion.StartModel.graph line 172
  20. lemma OAI.DiamondDistortion.StartModel.representation_norm_zero line 176
  21. lemma OAI.DiamondDistortion.StartModel.representation_norm_succ line 177
  22. lemma OAI.DiamondDistortion.StartModel.root_start_mass line 179
  23. lemma OAI.DiamondDistortion.StartModel.children_cost_sq line 181
  24. theorem OAI.DiamondDistortion.PathModel.quadratic_relative_graph line 191
  25. theorem OAI.DiamondDistortion.PathModel.quadratic_tail_seven_graph line 195
  26. theorem OAI.DiamondDistortion.PathModel.quadratic_pruning_graph line 199