English
There exists a function g equal to f at all places except possibly one, and the global product equals a prescribed B.
Русский
Существует функция g, совпадающая с f во всех местах кроме одного, и общий произведение равно заданному B.
LaTeX
$$$$ \exists g: \ InfinitePlace(K) \to NNReal,\; (\forall w\neq w_1, g(w)=f(w)) \land \prod_w g(w)^{mult(w)} = B. $$$$
Lean4
/-- This is a technical result: quite often, we want to impose conditions at all infinite places
but one and choose the value at the remaining place so that we can apply
`exists_ne_zero_mem_ringOfIntegers_lt`. -/
theorem adjust_f {w₁ : InfinitePlace K} (B : ℝ≥0) (hf : ∀ w, w ≠ w₁ → f w ≠ 0) :
∃ g : InfinitePlace K → ℝ≥0, (∀ w, w ≠ w₁ → g w = f w) ∧ ∏ w, (g w) ^ mult w = B := by
classical
let S := ∏ w ∈ Finset.univ.erase w₁, (f w) ^ mult w
refine ⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩
· exact fun w hw => Function.update_of_ne hw _ f
· rw [← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁), Function.update_self,
Finset.prod_congr rfl fun w hw => by rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)], ←
NNReal.rpow_natCast, ← NNReal.rpow_mul, inv_mul_cancel₀, NNReal.rpow_one, mul_assoc, inv_mul_cancel₀, mul_one]
· rw [Finset.prod_ne_zero_iff]
exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))
· rw [mult]; split_ifs <;> norm_num
