OAI/Analysis/DiamondDistortion/ModelMaps.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.DiamondDistortion.RecursiveModel.countableCoord line 16
  2. lemma OAI.DiamondDistortion.RecursiveModel.aggregate_sq line 21
  3. lemma OAI.DiamondDistortion.RecursiveModel.components_zero line 29
  4. lemma OAI.DiamondDistortion.RecursiveModel.outer_support line 37
  5. lemma OAI.DiamondDistortion.RecursiveModel.outer_sq line 44
  6. lemma OAI.DiamondDistortion.RecursiveModel.components_filter line 54
  7. lemma OAI.DiamondDistortion.RecursiveModel.outer_contractive line 65
  8. lemma OAI.DiamondDistortion.RecursiveModel.outer_orthogonal line 75
  9. lemma OAI.DiamondDistortion.RecursiveModel.energy_components line 97
  10. lemma OAI.DiamondDistortion.PathModel.path_norm line 116
  11. lemma OAI.DiamondDistortion.PathModel.linear_l2 line 121
  12. lemma OAI.DiamondDistortion.PathModel.finite_l2_sq line 131
  13. lemma OAI.DiamondDistortion.PathModel.linear_upper line 134
  14. lemma OAI.DiamondDistortion.PathModel.linear_lower line 145
  15. lemma OAI.DiamondDistortion.PathModel.linearBlocks line 168
  16. instance OAI.DiamondDistortion.PathModel.linearDualSeparable line 175
  17. theorem OAI.DiamondDistortion.PathModel.linear_weak_graph line 178

    Source documentation

    The original weak-sequence input on the concrete linear path-cost space.

    theorem linear_weak_graph (hinput : PathApplications.WeakInput LinearSpace)
    {D s : ℝ} (k : ℕ) (f : Diamond.Vertex k → LinearSpace) (hf : Diamond.HasDistortion k f D s) :
    1+(k:ℝ)/64 ≤ D^2 := PathApplications.weak_linear hinput k f hf
…

    Mentions: OAI.DiamondDistortion.PathApplications.WeakInput, OAI.DiamondDistortion.PathModel.LinearSpace, OAI.DiamondDistortion.Diamond.Vertex, OAI.DiamondDistortion.Diamond.HasDistortion, OAI.DiamondDistortion.PathApplications.weak_linear

  18. def OAI.DiamondDistortion.StartModel.ContractiveMap.lift line 189
  19. lemma OAI.DiamondDistortion.StartModel.ContractiveMap.lift_apply line 194
  20. lemma OAI.DiamondDistortion.StartModel.ContractiveMap.lift_norm line 196
  21. def OAI.DiamondDistortion.StartModel.ContractiveMap.prod₁ line 202
  22. lemma OAI.DiamondDistortion.StartModel.ContractiveMap.prod₁_norm line 205
  23. def OAI.DiamondDistortion.StartModel.ContractiveMap.single line 210
  24. abbrev OAI.DiamondDistortion.StartModel.rawRepresentationModel line 220

    Source documentation

    Repetition labels are retained: each start node admits a countable sequence of signed coefficient arrays over all its possible endpoints. Its mass is the ℓ¹ sum of the ℓ¹ norms of these arrays, before any cancellation.

    abbrev rawRepresentationModel : ℕ → RealNormed
  | 0 => ⟨lp (fun _ : ℕ => ℝ) 1⟩
  | h+1 => ⟨WithLp 1 (lp (fun _ : ℕ => L1 (h+1)) 1 ×
      lp (fun _ : ℕ => rawRepresentationModel h) 2)⟩

    Mentions: OAI.DiamondDistortion.StartModel.RealNormed

  25. abbrev OAI.DiamondDistortion.StartModel.Raw line 224
  26. def OAI.DiamondDistortion.StartModel.compression line 228

    Source documentation

    Group repetitions at every start/end pair. Triangle inequalities make this operation contractive, rather than an unjustified equality of costs.

    def compression : (h : ℕ) → {f : Raw h →ₗ[ℝ] Rep h // ∀ d,‖f d‖ ≤ ‖d‖}
  | 0 => ⟨(lp.tsumCLM ℝ ℕ ℝ).toLinearMap,lp.norm_tsum_le⟩
  | h+1 =>
    let prev := compression h
…

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

  27. def OAI.DiamondDistortion.StartModel.expansion line 240

    Source documentation

    A representation with no repetitions is also one of the arbitrary countable representations, by placing all its coefficients in repetition row zero.

    def expansion : (h : ℕ) → {f : Rep h →ₗ[ℝ] Raw h // ∀ d,‖f d‖ ≤ ‖d‖}
  | 0 => ContractiveMap.single ℝ
  | h+1 =>
    let prev := expansion h
…

    Mentions: OAI.DiamondDistortion.StartModel.Rep, OAI.DiamondDistortion.StartModel.Raw, OAI.DiamondDistortion.StartModel.ContractiveMap.single

  28. lemma OAI.DiamondDistortion.StartModel.tsum_single_zero line 250
  29. lemma OAI.DiamondDistortion.StartModel.compression_expansion line 257
  30. def OAI.DiamondDistortion.StartModel.rawOutput line 271

    Source documentation

    Literal coordinatewise output of countably many signed segments: first sum all rows with a common start/end, then use the absolutely summable path map.

    def rawOutput (h : ℕ) : Raw h →ₗ[ℝ] (Coord h → ℝ) :=
…

    Mentions: OAI.DiamondDistortion.StartModel.Raw

  31. def OAI.DiamondDistortion.StartModel.rawRelation line 274
  32. lemma OAI.DiamondDistortion.StartModel.raw_cost_eq line 283
  33. theorem OAI.DiamondDistortion.StartModel.finiteCost_eq_raw_sInf line 298

    Source documentation

    The start-cost infimum is unchanged when arbitrary repetitions are allowed. No minimizer, finite optimal representation, or attained infimum is assumed.

    theorem finiteCost_eq_raw_sInf (h : ℕ) (v : Vec h) :
    finiteCost h v=sInf {r : ℝ | ∃ d : Raw h,rawOutput h d=(fun s => v s) ∧ ‖d‖=r} := by
…

    Mentions: OAI.DiamondDistortion.StartModel.finiteCost, OAI.DiamondDistortion.StartModel.Raw, OAI.DiamondDistortion.StartModel.rawOutput

  34. lemma OAI.DiamondDistortion.StartModel.lp1_norm line 303
  35. lemma OAI.DiamondDistortion.StartModel.raw_norm_zero line 308
  36. lemma OAI.DiamondDistortion.StartModel.raw_root_mass line 312

    Source documentation

    The exact start masses before any grouping or cancellation.

    lemma raw_root_mass (h : ℕ) (d : Raw (h+1)) :
    ‖d.fst‖=∑' j,∑' s : Coord (h+1),|d.fst j s| := by
…

    Mentions: OAI.DiamondDistortion.StartModel.Raw

  37. lemma OAI.DiamondDistortion.StartModel.raw_children_cost_sq line 319
  38. lemma OAI.DiamondDistortion.StartModel.raw_norm_succ line 323
  39. lemma OAI.DiamondDistortion.StartModel.raw_root_absolute line 329

    Source documentation

    Absolute convergence of all root-start row outputs, at every coordinate. The rest of each coordinate's output is the finite ancestral recursion.

    lemma raw_root_absolute (h : ℕ) (d : Raw (h+1)) (r : Coord (h+1)) :
    Summable (fun j => ‖path (h+1) (d.fst j) r‖) := by
…

    Mentions: OAI.DiamondDistortion.StartModel.Raw

  40. lemma OAI.DiamondDistortion.StartModel.raw_root_tsum line 335