OAI/Geometry/TamingCompatibility/DifferentialForms/Kernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.FourierCutoff.pairing_modulate_eq_inverse line 23
2. def OAI.TamingCompatibility.FourierCutoff.kernel line 36
3. theorem OAI.TamingCompatibility.FourierCutoff.compact_inverse_cutoff line 42
4. lemma OAI.TamingCompatibility.FourierCutoff.inverse_cutoff_apply line 48
5. lemma OAI.TamingCompatibility.FourierIdentification.ae_eq_of_distribution_eq line 70
6. lemma OAI.TamingCompatibility.FourierIdentification.integral_inverse_smul_swap line 82
7. def OAI.TamingCompatibility.FourierIdentification.inverseTop line 92
8. lemma OAI.TamingCompatibility.FourierIdentification.inverseTop_coe line 96
9. lemma OAI.TamingCompatibility.FourierIdentification.inverseTop_to_distribution line 100
10. lemma OAI.TamingCompatibility.FourierIdentification.distribution_eq_of_ae_eq line 113
11. theorem OAI.TamingCompatibility.FourierIdentification.inverse_L1_L2 line 129