OAI/MeasureTheory/Falconer/Fourier/InverseJetValues.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Falconer.DescriptorJetSymbol.seedJet line 21
2. def OAI.Falconer.DescriptorJetSymbol.seedRadius line 25
3. def OAI.Falconer.DescriptorJetSymbol.seedMask line 29
4. theorem OAI.Falconer.DescriptorJetSymbol.seedMask_smooth line 36
5. theorem OAI.Falconer.DescriptorJetSymbol.seedRadius_pos line 47
6. theorem OAI.Falconer.DescriptorJetSymbol.seedProduct line 53
7. theorem OAI.Falconer.DescriptorJetSymbol.ambient_eq_seedProduct line 86
8. def OAI.Falconer.descriptorInverseSeparation line 98
9. theorem OAI.Falconer.descriptorInverseSeparation_left line 109
10. theorem OAI.Falconer.descriptorInverseSeparation_right line 156
11. theorem OAI.Falconer.DescriptorJetSymbol.value_normalized_angular_restore line 202

    Source documentation

    Restoring both normalization constants recovers the original spatial factor and every normalized descriptor jet exactly.

    theorem value_normalized_angular_restore {n K L : ℕ} {F : Finset PolicyDescriptor}
        {D : ℝ} (u : DescriptorJetSymbol n K L F D)
        (Q : DyadicCube (n+2)) (ρ : Measure (Space (n+2))) (profile : ℝ → ℝ)
        (N : ℕ) (σ : ℝ) (J i : ℕ) (S : PolicyDescriptor → Finset (Sphere (n+2)))
        {A B : ℝ} (hA : 0 < A) (hB : 0 < B) (q : Space (n+2) → ℂ)
        (hq : u.angular = normalizedAngular B q) (x : Space (n+2)) (w : Sphere (n+2)) :
        ((A*B : ℝ) : ℂ)*u.value Q ρ profile N σ J i S A x w =
          u.spatial x*q w*descriptorJetProduct Q ρ profile N σ J i F id S
            (fun b => (u.jet b).order) (fun b _ => (u.jet b).vectors) x w := by
    …

    Mentions: OAI.Falconer.DescriptorJetSymbol, OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.normalizedAngular, OAI.Falconer.descriptorJetProduct