OAI/Combinatorics/CliqueFree/Optimizer.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CliqueFreeIndependence.WeightedGraph.edgeForm line 17

    Source documentation

    The directed bilinear edge form (twice the quadratic mass on the diagonal).

    noncomputable def edgeForm (G : SimpleGraph V) (a b : V → ℝ) : ℝ :=
…
  2. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeForm_self line 20
  3. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeForm_symm line 24
  4. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeForm_add_left line 29
  5. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeForm_add_right line 40
  6. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeForm_neighbor line 44
  7. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_add line 48
  8. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeForm_mono line 55
  9. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_mono_weight line 66
  10. def OAI.CliqueFreeIndependence.WeightedGraph.spike line 72
  11. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeForm_spike line 74
  12. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_spike line 79
  13. lemma OAI.CliqueFreeIndependence.WeightedGraph.update_eq_add_spike line 89
  14. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_update line 94
  15. def OAI.CliqueFreeIndependence.WeightedGraph.vertexPotential line 100

    Source documentation

    The vertex summand, with Mathlib's log(0)=0 convention.

    def vertexPotential (t : ℝ) : ℝ := t * (1-Real.log t)
  16. def OAI.CliqueFreeIndependence.WeightedGraph.potential line 102
  17. def OAI.CliqueFreeIndependence.WeightedGraph.IsOptimizer line 105
  18. lemma OAI.CliqueFreeIndependence.WeightedGraph.continuous_vertexPotential line 108
  19. lemma OAI.CliqueFreeIndependence.WeightedGraph.continuous_edgeMass line 115
  20. lemma OAI.CliqueFreeIndependence.WeightedGraph.continuous_potential line 125
  21. lemma OAI.CliqueFreeIndependence.WeightedGraph.vertexPotential_le_one line 130
  22. lemma OAI.CliqueFreeIndependence.WeightedGraph.potential_clamp line 138
  23. lemma OAI.CliqueFreeIndependence.WeightedGraph.exists_optimizer line 150
  24. lemma OAI.CliqueFreeIndependence.WeightedGraph.potential_update line 161
  25. lemma OAI.CliqueFreeIndependence.WeightedGraph.optimizer_stationary line 179
  26. lemma OAI.CliqueFreeIndependence.WeightedGraph.optimizer_divergence line 219

    Source documentation

    Expansion around a stationary positive maximizer.

    lemma optimizer_divergence {G : SimpleGraph V} {w : V → ℝ} (hw : IsOptimizer G w)
    (q : V → ℝ) (hq : ∀ v, 0 ≤ q v) :
    0 ≤ potential G w - potential G q ∧
      potential G w - potential G q =
        (∑ v, (q v * Real.log (q v / w v) - q v + w v)) + edgeMass G (q-w) := by
…

    Mentions: OAI.CliqueFreeIndependence.WeightedGraph.IsOptimizer, OAI.CliqueFreeIndependence.WeightedGraph.potential, OAI.CliqueFreeIndependence.WeightedGraph.edgeMass