DescriptorJetRemoval.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Reached differentiated masks in positive independent energy

Every unreached occurrence remains in the endpoint transform. The cost of removing reached factors depends on the fixed total jet order, not on the number of undifferentiated masks or the scale.

def OAI.Falconer.descriptorJetBound line 16
theorem OAI.Falconer.descriptorJetBound_one_le line 19
theorem OAI.Falconer.descriptorJetProduct_norm_le line 22

theorem OAI.Falconer.descriptorJetProduct_fixed_measurable line 45

Source documentation

Evaluate the spatial parameter before proving angular measurability.

theorem descriptorJetProduct_fixed_measurable {d : ℕ} {ι : Type*}
    (Q : DyadicCube d) (ρ : Measure (Space d)) (m : ℝ → ℝ)
    (N : ℕ) (σ : ℝ) (J i : ℕ) (F : Finset ι)
    (b : ι → PolicyDescriptor) (S : PolicyDescriptor → Finset (Sphere d))
    (k : ι → ℕ) (v : (j : ι) → Sphere d → Fin (k j) → Space d)
    (hv : ∀ j ∈ F, Measurable (v j)) (x : Space d) :
    Measurable (fun w => descriptorJetProduct Q ρ m N σ J i F b S k v x w) := by
…

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

theorem OAI.Falconer.independentAngularEnergy_endpoint_remove_factors line 55

Source documentation

Bounded angular factors can be removed from two finite endpoint laws.

theorem independentAngularEnergy_endpoint_remove_factors {d : ℕ}
    (μ ν : Measure (Space d)) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    {M P : ℝ} (hM : 0 < M) (hP : 0 < P)
    (f g : Space d → Sphere d → ℂ)
    (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g))
    {C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hfC : ∀ x w, ‖f x w‖ ≤ C) (hgD : ∀ x w, ‖g x w‖ ≤ D)
    (p q : Sphere d → ℂ) (hp : Measurable p) (hq : Measurable q)
    {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hpA : ∀ w, ‖p w‖ ≤ A) (hqB : ∀ w, ‖q w‖ ≤ B)
    (a t : ℝ) (Ψ : ℝ → ℝ)
    [IsFiniteMeasure (PlanarFalconer.sourceAngularShellMeasure t Ψ)] :
…

Mentions: OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.PlanarFalconer.sourceAngularShellMeasure

theorem OAI.Falconer.endpointTransform_descriptorJetProduct_split line 81
theorem OAI.Falconer.independentAngularEnergy_descriptorJets_remove line 108