OAI/Analysis/WeakInfiniteness/NuclearApproximation.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakPureInfiniteness.tensorPolynomial_eq_sumline 35 - lemma
OAI.WeakPureInfiniteness.norm_cpTensor_comp_leline 42 - lemma
OAI.WeakPureInfiniteness.norm_cpTensor_sum_error_leline 52 - lemma
OAI.WeakPureInfiniteness.nuclear_tensor_approximationline 78