OAI/Combinatorics/CliqueFree/SplittingLoss.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.bad_survives line 27
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.bad_mass_le line 53
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.surviving_mass_eq line 79
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.expected_loss_le line 91

   Source documentation

   The finite-law aggregate of all corner and incidence losses.

   lemma expected_loss_le [Nonempty (EdgeState G)] {w : V → ℝ} (hw : ∀ u, 0 < w u)
       (hc : ∀ u v, G.Adj u v → 0 < commonMass G w u v)
       (K : Kernel (EdgeState G)) {q : (EdgeState G → EdgeState G) → ℝ}
       (hq : Law q) (hm : ∀ i y, (∑ F, if F i = y then q F else 0) = K i y)
       (hp : ∀ i j, (∑ F, if F i ≠ F j then q F else 0) ≤ 2 * tv (K i) (K j))
       (good : (EdgeState G → EdgeState G) → EdgeState G → Prop)
       (b : EdgeState G → EdgeState G → Prop)
       (hb : ∀ F e, good F e ↔ b e (F e)) :
       (∑ F, q F * ∑ t : TriangleState G, TriangleState.weight w t * bad (Survives F (good F) t)) ≤
         normalizer G w *
           (6 * (∑ e, law G w e * ∑ z, transition G w e z * tv (K e) (K z)) +
            6 * (∑ e, law G w e * ∑ y, K e y * bad (b e y))) := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.EdgeState, OAI.CliqueFreeIndependence.WeightedGraph.commonMass, OAI.CliqueFreeIndependence.WeightedGraph.TriangleState, OAI.CliqueFreeIndependence.WeightedGraph.TriangleState.weight, OAI.CliqueFreeIndependence.WeightedGraph.Splitting.Survives

5. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.exists_graph line 158

   Source documentation

   Splitting from a joint kernel preserving first coordinates, with two averaged losses.

   lemma exists_graph [Nonempty (EdgeState G)] {w : V → ℝ} (hw : ∀ u, 0 < w u)
       (hc : ∀ u v, G.Adj u v → 0 < commonMass G w u v)
       (K : Kernel (EdgeState G)) (hK : Stochastic K)
       (hblock : ∀ e z, e.src ≠ z.src → K e z = 0)
       {a D δ : ℝ}
       (hD : (∑ e, law G w e * ∑ z, transition G w e z * tv (K e) (K z)) ≤ D)
       (hδ : (∑ e, law G w e * ∑ y,
         if K y e < w e.dst * Real.exp (-a) then K e y else 0) ≤ δ) :
       ∃ H : SimpleGraph (EdgeState G), EdgeProjection H G EdgeState.src ∧
         (∀ z, neighborMass H (w ∘ EdgeState.src) z ≤ Real.exp a) ∧
         (1 - 6 * D - 6 * δ) * triangleMass G w ≤ triangleMass H (w ∘ EdgeState.src) := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.EdgeState, OAI.CliqueFreeIndependence.WeightedGraph.commonMass, OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection, OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.src, OAI.CliqueFreeIndependence.WeightedGraph.neighborMass, OAI.CliqueFreeIndependence.WeightedGraph.triangleMass