Trust

Axioms come from the Lean kernel (Lean (version 4.35.0-rc4, x86_64-w64-windows-gnu, commit c29b6dda4f7c20e3eeaa717c4e565663c5cfa364, Release)): the constants each declaration depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.

Lake environment and dependency-pin digest: 53884547f5da0119.

Verification scope: all declaration-bearing files; 70 of 70 eligible files selected, 1027 declarations requested.

Rendering mode: clean content-bound cache results only; 0 selected files had no reusable result and remain UNKNOWN. No Lean process was started for those misses during this static-site build.

Per-file probe bounds: 300 seconds. A resource stop is UNKNOWN, never a failed proof.

no axioms

12

standard axioms

973

sorry

6

extra axioms

0

unknown

36

What the badges mean

no axioms

Lean's kernel checked the proof, and it rests on nothing but Lean's rules.

standard axioms

Checked by the kernel, using only propext, Classical.choice or Quot.sound: the three axioms nearly all of mathematics in Lean uses.

extra axioms

Checked by the kernel, but it assumes something the project declared with `axiom`. It is only as true as those assumptions.

depends on sorry

Not proved: somewhere in it, or in something it uses, a proof was left out (`sorry`).

trust unknown

Lean did not check it: Lean was not run, the file did not elaborate, or Lean has no constant by that name.

Trust UNKNOWN declarations (36)

1. hmeas2 PFR/Endgame.lean trust unknown: Lean has no constant by this name
2. ProbabilityTheory._root_.MeasureTheory.Measure.support PFR/ForMathlib/Entropy/Measure.lean trust unknown: Lean has no constant by this name
3. ProbabilityTheory.iIndepFun.κ PFR/ForMathlib/FourVariables.lean trust unknown: Lean has no constant by this name
4. ProbabilityTheory.iIndepFun.κ_equiv PFR/ForMathlib/FourVariables.lean trust unknown: Lean has no constant by this name
5. ProbabilityTheory.iIndepFun.fintype_kappa PFR/ForMathlib/FourVariables.lean trust unknown: Lean has no constant by this name
6. ProbabilityTheory.iIndepFun.κ PFR/ForMathlib/ThreeVariables.lean trust unknown: Lean has no constant by this name
7. ProbabilityTheory.iIndepFun.κ_equiv PFR/ForMathlib/ThreeVariables.lean trust unknown: Lean has no constant by this name
8. ProbabilityTheory.iIndepFun.fintype_kappa PFR/ForMathlib/ThreeVariables.lean trust unknown: Lean has no constant by this name
9. ProbabilityTheory.iIndepFun.self_or_prod PFR/ForMathlib/ThreeVariables.lean trust unknown: Lean has no constant by this name
10. ProbabilityTheory._root_.MeasureTheory.MeasurePreserving.identDistrib PFR/Mathlib/Probability/IdentDistrib.lean trust unknown: Lean has no constant by this name
11. ProbabilityTheory._root_.Finset.prod_univ_prod PFR/Mathlib/Probability/Independence/Basic.lean trust unknown: Lean has no constant by this name
12. ProbabilityTheory._root_.Finset.prod_univ_prod' PFR/Mathlib/Probability/Independence/Basic.lean trust unknown: Lean has no constant by this name
13. ProbabilityTheory.Kernel._root_.MeasureTheory.Measure.compProd_apply_singleton PFR/Mathlib/Probability/Kernel/Disintegration.lean trust unknown: Lean has no constant by this name
14. ProbabilityTheory.Kernel._root_.MeasureTheory.Measure.ae_of_compProd_eq_zero PFR/Mathlib/Probability/Kernel/Disintegration.lean trust unknown: Lean has no constant by this name
15. ProbabilityTheory.Kernel._root_.MeasureTheory.Measure.ae_of_ae_compProd PFR/Mathlib/Probability/Kernel/Disintegration.lean trust unknown: Lean has no constant by this name
16. entropy_kvm_step PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
17. entropy_sum_le_entropy_neg_add PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
18. kvm_decomposition_indep_helper PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
19. entropy_kvm_decomposition PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
20. Finset.prod_mul PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
21. mes_of_comap PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
22. ident_of_cond_of_indep PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
23. prob_nonzero_of_prod_prob_nonzero PFR/MoreRuzsaDist.lean trust unknown: Lean has no constant by this name
24. rhoMinus_continuous_aux1 PFR/RhoFunctional.lean trust unknown: Lean has no constant by this name
25. rhoMinus_continuous_aux2 PFR/RhoFunctional.lean trust unknown: Lean has no constant by this name
26. rhoMinus_continuous_aux3 PFR/RhoFunctional.lean trust unknown: Lean has no constant by this name
27. le_rhoMinus_of_subgroup PFR/RhoFunctional.lean trust unknown: Lean has no constant by this name
28. rhoMinus_le_of_subgroup PFR/RhoFunctional.lean trust unknown: Lean has no constant by this name
29. rho_le_translate PFR/RhoFunctional.lean trust unknown: Lean has no constant by this name
30. Mathlib.Tactic.RPowRing._root_.Real.pow_neg PFR/Tactic/RPowSimp.lean trust unknown: Lean has no constant by this name
31. Mathlib.Tactic.RPowRing._root_.Real.inv_rpow' PFR/Tactic/RPowSimp.lean trust unknown: Lean has no constant by this name
32. Mathlib.Tactic.RPowRing._root_.Real.rpow_inv PFR/Tactic/RPowSimp.lean trust unknown: Lean has no constant by this name
33. Marton.pfr_conjecture_aux PFRPalomar/Solution.lean trust unknown: Lean has no constant by this name
34. Marton.pfr_conjecture_nine_aux PFRPalomar/Solution.lean trust unknown: Lean has no constant by this name
35. Marton.homomorphism_pfr_aux PFRPalomar/Solution.lean trust unknown: Lean has no constant by this name
36. Marton.approx_hom_pfr_aux PFRPalomar/Solution.lean trust unknown: Lean has no constant by this name

Depend on sorry (6)

1. Marton.pfr_conjecture PFRPalomar/Challenge.lean
2. Marton.pfr_conjecture_nine PFRPalomar/Challenge.lean
3. Marton.torsion_pfr_conjecture PFRPalomar/Challenge.lean
4. Marton.weak_pfr_int PFRPalomar/Challenge.lean
5. Marton.homomorphism_pfr PFRPalomar/Challenge.lean
6. Marton.approx_hom_pfr PFRPalomar/Challenge.lean