pith. machine review for the scientific record. sign in
theorem proved tactic proof

variational_step_unique

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 290theorem variational_step_unique {N : ℕ} (hN : 0 < N)
 291    (c : Configuration N)
 292    (next₁ next₂ : Configuration N)
 293    (h₁ : IsVariationalSuccessor c next₁)
 294    (h₂ : IsVariationalSuccessor c next₂) :
 295    next₁.entries = next₂.entries := by

proof body

Tactic-mode proof.

 296  have h_uniform : IsVariationalSuccessor c (constant_config (log_charge c / N) : Configuration N) := by
 297    constructor
 298    · show log_charge (constant_config (log_charge c / N) : Configuration N) = log_charge c
 299      rw [constant_config_log_charge]
 300      exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
 301    · intro c' hc'
 302      rw [constant_config_total_defect]
 303      have hbound := total_defect_lower_bound hN c'
 304      rw [hc'] at hbound
 305      exact hbound
 306  have h1_eq_min : total_defect next₁ = (N : ℝ) * Jlog (log_charge c / N) := by
 307    have h1le := h₁.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
 308    have h1ge := h_uniform.2 next₁ h₁.1
 309    rw [constant_config_total_defect] at h1le h1ge
 310    exact le_antisymm h1le h1ge
 311  have h2_eq_min : total_defect next₂ = (N : ℝ) * Jlog (log_charge c / N) := by
 312    have h2le := h₂.2 (constant_config (log_charge c / N) : Configuration N) h_uniform.1
 313    have h2ge := h_uniform.2 next₂ h₂.1
 314    rw [constant_config_total_defect] at h2le h2ge
 315    exact le_antisymm h2le h2ge
 316  have h1_const :
 317      next₁.entries = (constant_config (log_charge next₁ / N) : Configuration N).entries := by
 318    apply eq_constant_config_of_defect_eq hN next₁
 319    rw [← h₁.1] at h1_eq_min
 320    exact h1_eq_min
 321  have h2_const :
 322      next₂.entries = (constant_config (log_charge next₂ / N) : Configuration N).entries := by
 323    apply eq_constant_config_of_defect_eq hN next₂
 324    rw [← h₂.1] at h2_eq_min
 325    exact h2_eq_min
 326  have hcharge1 : log_charge next₁ = log_charge c := h₁.1
 327  have hcharge2 : log_charge next₂ = log_charge c := h₂.1
 328  calc
 329    next₁.entries = (constant_config (log_charge next₁ / N) : Configuration N).entries := h1_const
 330    _ = (constant_config (log_charge c / N) : Configuration N).entries := by rw [hcharge1]
 331    _ = (constant_config (log_charge next₂ / N) : Configuration N).entries := by rw [hcharge2]
 332    _ = next₂.entries := h2_const.symm
 333
 334/-! ## Defect Reduction -/
 335
 336/-- **Theorem (Variational Step Reduces Defect)**:
 337    The total defect of the successor is at most the total defect
 338    of the current state.
 339
 340    This follows immediately: the current state is feasible for itself,
 341    and the successor minimizes over the feasible set, so the successor's
 342    cost is at most the current state's cost. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (32)

Lean names referenced from this declaration's body.

… and 2 more