Mathematics · proofs · software

Special Functions · Lean source

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

CoupledAnalyticAudit.lean23 lines

Original source pathlean/CoupledAnalyticAudit.lean

Skip source text

1 import CoupledAnalytic
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_zero
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_neg
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_series_uniform_bound
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn_ball
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.exists_local_radius
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableAt
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_differentiableOn
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddTerm_hasDerivAt
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasSum_deriv
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_hasDerivAt
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_bounds_left
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coefficient_bounds_right
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_differentiableOn
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.mul_mem_localDisk
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_mul_eq
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.nextCoefficient_mul_denominator
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.oddSum_deriv_eq_of_recurrence
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_local_equations
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_local_solution
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_initial_derivatives
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.coupled_odd

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: 24327e3a8365da563fb7c654ecf379d9ec14ac5d137c3a5a27a00b883bf12051

Original source on GitHub

Back to Special Functions