OAI/InformationTheory/AmplitudeDamping/OutputConvexity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GAD.radius line 22
2. def OAI.GAD.logRatio line 23
3. def OAI.GAD.wootters line 24
4. def OAI.GAD.woottersSlope line 25
5. theorem OAI.GAD.continuous_g line 27
6. theorem OAI.GAD.continuous_wootters line 31
7. theorem OAI.GAD.radius_pos_lt_one line 35
8. theorem OAI.GAD.radius_sq line 42
9. theorem OAI.GAD.logRatio_lower line 47
10. theorem OAI.GAD.hasDerivAt_radius line 57
11. theorem OAI.GAD.binEntropy_derivative_radius line 66
12. theorem OAI.GAD.hasDerivAt_wootters line 77
13. theorem OAI.GAD.hasDerivAt_logRatio line 89
14. theorem OAI.GAD.hasDerivAt_woottersSlope line 102
15. theorem OAI.GAD.deriv_wootters line 118
16. theorem OAI.GAD.deriv2_wootters line 121
17. theorem OAI.GAD.convexOn_wootters line 129
18. theorem OAI.GAD.monotoneOn_wootters line 147
19. theorem OAI.GAD.v_nonneg line 160
20. theorem OAI.GAD.v_population_form line 166
21. theorem OAI.GAD.v_le_quarter line 172
22. theorem OAI.GAD.sqrt_v_mem line 180
23. theorem OAI.GAD.convexOn_sqrt_v line 187
24. theorem OAI.GAD.wootters_sqrt line 218
25. theorem OAI.GAD.convexOn_output_entropy line 223
26. theorem OAI.GAD.continuous_objective line 237
27. theorem OAI.GAD.exists_maximizer line 243

    Source documentation

    Existence of the genuine scalar maximum rather than a supremum surrogate.

    theorem exists_maximizer (γ ν : ℝ) :
        ∃ p ∈ Icc (0 : ℝ) 1, ∀ q ∈ Icc (0 : ℝ) 1, objective γ ν q ≤ objective γ ν p := by
    …

    Mentions: OAI.GAD.objective