Continuity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Boundary lower semicontinuity of maximum entropy and attainment of the entropy defect.

theorem OAI.MatchingEntropy.maxMatchingEntropy_mix_ge line 21

Source documentation

Concavity of H follows from mixing genuine optimizing probability laws.

theorem maxMatchingEntropy_mix_ge (G : LooplessGraph V E) {x y : E → ℝ}
    (hx : x ∈ G.polytope) (hy : y ∈ G.polytope) {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    (1-t)*maxMatchingEntropy G x+t*maxMatchingEntropy G y ≤
      maxMatchingEntropy G ((1-t) • x+t • y) := by
…

Mentions: OAI.MatchingEntropy.maxMatchingEntropy

theorem OAI.MatchingEntropy.maxMatchingEntropy_lowerSemicontinuousOn line 39
Source documentation
Boundary lower semicontinuity, using the finite matching-polytope constraints. A fixed small mixing coefficient suffices for each prescribed entropy tolerance.
```
theorem maxMatchingEntropy_lowerSemicontinuousOn (G : LooplessGraph V E)
    (heven : Even (Fintype.card V)) :
    LowerSemicontinuousOn (maxMatchingEntropy G) G.polytope := by
…
```
Mentions: OAI.MatchingEntropy.maxMatchingEntropy

theorem OAI.MatchingEntropy.entropyDefect_attains_max line 63

Source documentation

The actual entropy defect attains a maximum on the closed matching polytope.

theorem entropyDefect_attains_max (G : LooplessGraph V E)
    (heven : Even (Fintype.card V)) (hPM : Nonempty G.Matching) (m : ℝ) :
    ∃ x ∈ G.polytope, ∀ y ∈ G.polytope, entropyDefect G m y ≤ entropyDefect G m x := by
…

Mentions: OAI.MatchingEntropy.entropyDefect