MovingSymmetrizedMaskedEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The bulk-averaged masked energy under the original restored prior

def OAI.Ostmann.movingSymmetrizedMaskedTemplateEnergy line 10
theorem OAI.Ostmann.movingSymmetrizedMaskedTemplateKernel_nonneg line 24

theorem OAI.Ostmann.movingSymmetrizedMaskedTemplateEnergy_weight_le line 41

Source documentation

A bound on the original support suffices: no support is conditioned into or removed from the independent restored law.

theorem movingSymmetrizedMaskedTemplateEnergy_weight_le
    (P Pg I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (outside : List ℕ) (μ : ℕ → P → ℝ)
    (hμ : ∀ j a, 0 ≤ μ j a)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
    (φ : ℝ → ℝ) (hφ : ∀ t, 0 ≤ φ t) (G : ℕ → ℝ) (n r m : ℕ)
    (Q : MovingRegularSlot n r m → Finset ℕ) (greg : ∀ q : ℕ, ZMod q → ℂ)
    (weight : (MovingRegularSlot n (4 + r) m → P) → ℝ) (B : ℝ)
    (hweight : ∀ x, (∏ i, movingTemplateRestoredPrior n r m (μ n)
      (fun i => primeSubsetPrior P (Q i)) i (x i)) ≠ 0 → weight x ≤ B) :
    movingSymmetrizedMaskedTemplateEnergy P Pg I hP outside μ childBound pivotBound V F φ G n r m Q greg weight ≤
      B * movingSymmetrizedMaskedTemplateEnergy P Pg I hP outside μ childBound pivotBound V F φ G n r m Q greg (fun _ => 1) := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateRestoredPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.movingSymmetrizedMaskedTemplateEnergy