OAI/Analysis/Conductivity/Sources/WeightedSpectralSpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ScalarConductivity.SpectralL2 line 11
2. abbrev OAI.ScalarConductivity.SpectralJet line 12
3. def OAI.ScalarConductivity.spectralTraceGraph line 14
4. lemma OAI.ScalarConductivity.spectralTraceGraph_closed line 26
5. instance OAI.ScalarConductivity.spectralTraceGraph_complete line 35
6. lemma OAI.ScalarConductivity.spectralTraceGraph_fst_injective line 38
7. lemma OAI.ScalarConductivity.sqrt_weight_norm_sq line 50
8. lemma OAI.ScalarConductivity.spectralTraceGraph_exists_iff line 56