Mathematics · proofs · software

Special Functions · Lean source

CoupledEntireAudit.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)

CoupledEntireAudit.lean21 lines

Original source pathlean/CoupledEntireAudit.lean

Skip source text

1 import CoupledEntire
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddConvolution_eq
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.next_term_mul_denominator
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.next_term_norm_le
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_series_bootstrap
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_bootstrap
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.maxScale_bounds
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.maxScale_lt_one
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_on_ladder
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_series_entire
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_term_norm_le_radius
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn_of_radius
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv_of_radius
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_entire_of_norm_summable
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv_entire
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.next_derivative_term_eq
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_entire_equation
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_equations
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_entire_solution

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: 26d045313a9af0ba5dba699fb3b4a87403824f5cbfb1fc5778009d16fc3233de

Original source on GitHub

Back to Special Functions