Mathematics · proofs · software

Special Functions · Lean source

CoupledEvaluationAudit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Local imports (1)

CoupledEvaluationAudit.lean38 lines

Original source pathlean/CoupledEvaluationAudit.lean

Skip source text

1 import CoupledEvaluation
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_real_hasSum
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_norm_summable
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_real_nonneg
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_real_mono
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_at_real
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_le_pairMax
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.realPairMax_nonneg
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.realPairMax_recurrence
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_coefficient_le_one
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_small_disk_bound
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.pair_small_disk_bound
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.diskMajorant_of_small
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.pair_le_diskMajorant
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.exists_diskMajorant_fuel
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_disk_majorant
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.disk_majorant_exists
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.outer_power_comparison
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.positive_odd_outer_remainder
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddPolynomial_at_real
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_outer_remainder
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_ladder_remainder
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_polynomial_le_component
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_evaluation_enclosure
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_ladder_enclosure
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rationalDiskMajorant_cast
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_disk_majorant_sound
29 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_outer_remainder
30 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_real_enclosure
31 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_coefficients_cast
32 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_component_coefficient_cast
33 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_polynomial_cast
34 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_maxScale_cast
35 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_fuel_exists
36 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rational_endpoint_enclosure
37 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_last_thirty_tail_rational
38 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unequal_last_thirty_error

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 5eac0617b6c36c875a5da3f43aa8ca9e484aea17d84ea5f15720358ee2f3c972

Original source on GitHub

Back to Special Functions